Switch from Azure Pipeline to Github Actions.

Minimize infrastructure dependencies.

.github/workflows/main.yml

@@ -0,0 +1,40 @@
+name: CI
+
+on: [push]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up JDK 1.8
+      uses: actions/setup-java@v1
+      with:
+        java-version: 1.8
+    - name: Get current date
+      id: date
+      run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
+    - name: Build with Ant
+      run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
+    - name: Create Release
+      id: create_release
+      uses: actions/create-release@v1
+      env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      with:
+        tag_name: ${{steps.date.outputs.date}}
+        release_name: ${{steps.date.outputs.date}}
+        draft: false
+        prerelease: false
+    - name: Upload Release Asset
+      id: upload-release-asset 
+      uses: actions/[email protected]
+      env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      with:
+        upload_url: ${{ steps.create_release.outputs.upload_url }}
+        asset_path: dist/CommunityModules-${{steps.date.outputs.date}}.jar
+        asset_name: CommunityModules-${{steps.date.outputs.date}}.jar
+        asset_content_type: application/zip

build.xml

@@ -6,6 +6,12 @@
 	<property name="lib" location="lib"/>
 	<property name="tests" location="tests"/>
 
+	<tstamp>
+		<format property="timestamp"
+          pattern="yyyyMMdHHmm"
+          locale="en,UK"/>
+	</tstamp>
+
 	<target name="init" description="Create the build and dist directory structure">
 		<mkdir dir="${build}"/>
 		<mkdir dir="${dist}"/>
@@ -25,7 +31,7 @@
 
 	<target name="dist" depends="compile" description="Combine the module overwrites and the TLA+ definitions into a distribution">
 		<tstamp/>
-		<jar jarfile="${dist}/CommunityModules-${DSTAMP}${TSTAMP}.jar">
+		<jar jarfile="${dist}/CommunityModules-${timestamp}.jar">
 			<fileset dir="${build}/"
              includes="**/*.class"/>
 			<fileset dir="${src}/"
@@ -50,7 +56,7 @@
 			<classpath>
 				<pathelement location="${lib}/tla2tools.jar" />
 				<!-- The jar that has just been built by the dist target. -->
-				<pathelement location="${dist}/CommunityModules-${DSTAMP}${TSTAMP}.jar" />
+				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
 			</classpath>
 		</java>
 	</target>

modules/IOUtils.tla

@@ -10,3 +10,28 @@ IOSerialize(val, absoluteFilename, compress) == TRUE
 IODeserialize(absoluteFilename, compressed) == CHOOSE val : TRUE
 
 ============================================================================
+
+\* Writes a TLA+ expression to the given file.
+\* TODO: Decide if it should write a module preamble.
+\* Write is easier to implement than Read because it goes from (valid) TLA+
+\* and writes a file whereas Read has to parse it.
+IOWrite(exp, absoluteFilename) == TRUE
+
+\* Reads a TLA+ expression from a file.
+\* TODO: Decide if it reads just a string from a file or expects (valid) TLA+.
+\*         For trace validation it would be preferable to read strings.
+\*       Constant-level expression (what's a use-case to read fileS during state space exploration?
+IORead(absoluteFilename) == TRUE
+
+TLAParse(IORead("C:\\foo\bar"))
+
+(* condition generally of level up to action (but not temporal), e.g. Inv'.  *)
+
+\* Run the given OS command if condition evaluates to true.
+\* This is novel and cannot be done otherwise.
+\* TODO: What to pass to os command? osCommand a string that a user munges directly
+\*       in/with TLA+.
+\*       Can IOWrite/IORead be spec'ed with IOExec?
+IOExec(condition, osCommand) == TRUE
+
+=============================================================================