Merge pull request #145 from UBC-NSS/fhackett-readme-and-ci

Bring README up to date, bring CI back to old glory

.github/workflows/ci.yml

@@ -8,19 +8,28 @@ on:
 
 jobs:
   build:
-
     runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        java-version: ['11', '12', '13', '14', '15', '16']
+        golang-version: ['1.13', '1.14', '1.15', '1.16']
 
     steps:
     - uses: actions/checkout@v2
-    - name: Set up JDK 11
+    - name: Set up JDK ${{ matrix.java-version }}
       uses: actions/setup-java@v2
       with:
-        java-version: '11'
+        java-version: ${{ matrix.java-version }}
         distribution: 'adopt'
     - name: Setup Go environment
       uses: actions/[email protected]
       with:
-        go-version: 1.14
+        go-version: ${{ matrix.golang-version }}
     - name: Run tests
       run: sbt test
+    - name: 'Upload Fuzz Test Results on Test Failure (in case there are some)'
+      if: ${{ failure() }}
+      uses: actions/upload-artifact@v2
+      with:
+        name: fuzz-test-results
+        path: fuzz_output/*

README.md

@@ -1,10 +1,15 @@
 # PGo ![CI Status](https://github.com/UBC-NSS/pgo/actions/workflows/ci.yml/badge.svg?branch=master)
 
-PGo is a source to source compiler to compile
-[PlusCal](http://lamport.azurewebsites.net/tla/pluscal.html)
-specifications into [Go](https://golang.org/) programs.
+PGo is a source to source compiler to compile Modular Pluscal
+specifications (whuch use a superset of
+[PlusCal](http://lamport.azurewebsites.net/tla/pluscal.html)) into [Go](https://golang.org/) programs.
 
-## Purpose/motivation
+In addition to the PGo compiler, this source tree includes:
+
+- the `distsys` support library, which is used by PGo's generated Go code, available in the `distsys/` folder.
+- syntax highlighting modes for Visual Studio Code and pygments, available in the `syntax/` folder.
+
+## Purpose and motivation
 
 [PlusCal](http://lamport.azurewebsites.net/tla/pluscal.html) is a
 language for specifying/modeling concurrent systems. It was designed
@@ -22,76 +27,115 @@ developing distributed systems.
 Currently there are no tools that correspond a PlusCal/TLA+ spec with
 an implementation of the spec. PGo is a tool that aims to connect the
 specification with the implementation by generating Go code based on a
-PlusCal specification. PGo enables the translation of a verified
-PlusCal specification of a distributed system algorithm into a
-semantically equivalent Go program.
+specification written in Modular PlusCal. The "Modular" prefix
+comes from the need to distinguish the description of a system from
+the model of its environment, which is needed for model checking.
+PGo enables the translation of a Modular PlusCal description of a
+distributed system to verifiable PlusCal,
+as well as to a semantically equivalent Go program.
 
 ## Current status
 
-Actively under development. PGo supports compilation of most
-uni-process and very simple multiprocess PlusCal algorithms into
-corresponding compilable and runnable Go code.
+Actively under development. PGo supports compilation of all PlusCal
+control flow constructs, but not procedures.
+PGo also supports a vast majority of the value-level TLA+ supported by TLC.
 
-See [`manual.pdf`](https://github.com/UBC-NSS/pgo/blob/master/manual.pdf) in the
+See [`manual.pdf`](https://github.com/UBC-NSS/pgo/blob/master/manual.pdf) (WARNING: update in progress) in the
 repository for a snapshot of the latest version of the manual that details
 implemented features and several examples.
 
 ## Usage
 
-To learn how to use PGo, see the [PGo usage page](https://github.com/UBC-NSS/pgo/wiki/PGo-Usage).
+To learn how to use PGo during verification, see the [PGo usage page](https://github.com/UBC-NSS/pgo/wiki/PGo-Usage) (WARNING: update in progress).
 
-## How it works
+For an in-depth description of how PGo works and how to interact with its generated code, see the manual (WARNING: update in progress).
 
-PGo is a source to source compiler written in Java. It compiles specifications written in an extension of PlusCal, called Modular PlusCal (see the [Modular PlusCal page](https://github.com/UBC-NSS/pgo/wiki/Modular-PlusCal) for more details), to Go programs.
+For the tool's compilation modes and flags at a high level, see below.
 
-## How to install (for development)
+The PGo tool's help text reads:
 
-Requirements: IntelliJ, Eclipse, or Ant 1.9
+```
+PGo compiler
+  -h, --help   Show help message
+
+Subcommand: gogen
+  -o, --out-file  <arg>
+  -p, --package-name  <arg>
+  -s, --spec-file  <arg>
+  -h, --help                  Show help message
+
+Subcommand: pcalgen
+  -s, --spec-file  <arg>
+  -h, --help               Show help message
+```
 
-First download/clone the repository
+### gogen
 
-Option 1: Import as an IntelliJ project.
+The `gogen` subcommand requests that PGo generate a Go file from an MPCal-containing TLA+ module.
+Most customisation of this stage should be done by choosing specific parameters when calling the generated Go code,
+so there are only a few options to consider.
 
-Option 2: Import as an Eclipse project.
+- `--out-file` specifies the path to the Go output file, like `-o` in GCC.
+- `--spec-file` specifies the path to the TLA+ input file
+- `--package-name` allows customisation of the package name of the Go output file. This defaults to a sanitized version of the
+  MPCal algorithm name.
 
-Option 3: Execute `ant build` to compile the project and then execute `pgo.sh [options] pcalfile` to compile `pcalfile`.
+### pcalgen
 
-Dependencies:
+The `pcalgen` subcommand requests that PGo rewrite its MPCal-containing TLA+ input file,
+such that it contains a PlusCal translation of the MPCal algorithm.
+The only option, `--spec-file`, is the path to the spec file, which will be rewritten.
 
-- The [Plume options library](https://mernst.github.io/plume-lib/).
+To insert the PlusCal translation, PGo will look for comments like, give or take whitespace:
+```
+\* BEGIN PLUSCAL TRANSLATION
+... any number of lines may go here
+\* END PLUSCAL TRANSLATION
+```
 
-- [Java Hamcrest](http://hamcrest.org/JavaHamcrest/).
+If it cannot find one of both of these comments in that order, it will give up with an error message describing the problem,
+and will not write any output.
 
-- The [JSON reference implementation](https://github.com/stleary/JSON-java).
+## How it works
 
-PGo is tested using OpenJDK 1.8, and 1.9, and Go 1.8, 1.9, 1.10, and 1.11.
+PGo is a source to source compiler written in Scala. It compiles specifications written in an extension of PlusCal,
+called Modular PlusCal (see the [Modular PlusCal page](https://github.com/UBC-NSS/pgo/wiki/Modular-PlusCal) for more details),
+to Go programs.
 
-## How to run (for development)
+## How to build (for development)
 
-Use `pgo.sh` to invoke the compiler. Below are the options that the compiler accepts.
+PGo's Scala code builds via an [sbt](https://www.scala-sbt.org/) project, with its dependencies managed
+by [Maven](https://maven.apache.org/).
+PGo additionally provides a runtime support library for its generated Go code, which lives in the `distsys/`
+subfolder. This Go code is a standard Go module, which can be imported via the URL https://github.com/UBC-NSS/pgo/distsys.
 
-```bash
-Usage: pgo [options] spec
-  --version=<boolean>          - Version [default false]
-  -h --help=<boolean>          - Print usage information [default false]
-  -q --logLvlQuiet=<boolean>   - Reduce printing during execution [default false]
-  -v --logLvlVerbose=<boolean> - Print detailed information during execution  [default false]
-  -m --mpcalCompile=<boolean>  - Compile a Modular PlusCal spec to vanilla PlusCal [default false]
-  -c --configFilePath=<string> - path to the configuration file, if any
-```
+The main build script is the top-level [build.sbt](https://github.com/UBC-NSS/pgo/blob/master/build.sbt).
+To build from terminal, run `sbt` in the root directory and use the standard commands provided by the sbt console.
+These include `run <command-line args>` to (re-)compile and run PGo, and `test` to run all tests, including Go tests
+(TODO: add runner for free-standing Go tests; that one, specifically, is missing).
+
+The sbt build can also be auto-imported by the IntelliJ Scala plugin, as well as likely any other IDE with Scala support.
+
+PGo's Scala code has managed dependencies on a small set of utility libraries:
+
+- [scallop](https://github.com/scallop/scallop) for command-line argument parsing
+- [scala-parser-combinators](https://github.com/scala/scala-parser-combinators) for the TLA+/PCal/MPCal parser
+- [os-lib](https://github.com/com-lihaoyi/os-lib) for simplified file and process manipulation (process manipulation is used during tests)
+
+PGo's test suites additionally depend on:
 
-## Further notes for developers
+- the `go` executable. The tests will attempt to find this, probably on the `$PATH` or equivalent, via the JVM's default lookup process.
+- [ScalaTest](https://www.scalatest.org/) as test framework
+- [ScalaCheck](https://www.scalacheck.org/) for implementing fuzz tests
+- [java-diff-utils](https://github.com/java-diff-utils/java-diff-utils) for generating diffs when tests compare big blocks of text
 
-If you use Eclipse, you should import the code style found in the
-`pgo-code-style.epf` file by clicking `File -> Import...` and
-selecting the file.
+PGo's Go runtime library depends on:
 
-Furthermore, use the Unix text file line delimiter (especially
-important if you are using Windows) by going to Eclipse's
-preferences/options, and under General and Workspace set "New text
-file line delimiter" to be "Unix".
+- [immutable](https://github.com/benbjohnson/immutable) for efficient immutable implementations of lists and maps in the TLA+ data model.
+  For example, creating a modified map with one different key-value pair should take constant time, rather than copy the
+  entire existing structure.
 
-By default Eclipse does not enable assertions. Our projects assume
-that you have assertions enabled at all times.  To globally enable
-assertions as a default for all projects, go to Window -> Preferences
--> Java / Installed JREs.  Select the JRE and click "Edit...".
+PGo is tested using OpenJDK 1.11 through 1.16, and Go 1.13 through 1.16.
+OpenJDK 1.11+ is needed because of standard API usage.
+Go >=1.13 is needed because of [changes to the errors package in that version](https://blog.golang.org/go1.13-errors),
+and, otherwise, Go >=1.11 is needed due to the use of Go modules.

build.sbt

@@ -10,7 +10,6 @@ Test / scalaSource := baseDirectory.value / "test"
 libraryDependencies += "org.scala-lang" % "scala-reflect" % scalaVersion.value
 
 libraryDependencies += "org.rogach" %% "scallop" % "4.0.2"
-libraryDependencies += "io.spray" %%  "spray-json" % "1.3.6"
 
 libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.2.0-M1"
 libraryDependencies += "com.lihaoyi" %% "os-lib" % "0.7.3"

distsys/go.mod

@@ -1,5 +1,5 @@
 module github.com/UBC-NSS/pgo/distsys
 
-go 1.14
+go 1.13
 
 require github.com/benbjohnson/immutable v0.3.0

distsys/tlaplus.go

@@ -201,7 +201,7 @@ func (v TLAValue) ApplyFunction(argument TLAValue) TLAValue {
 	switch data := v.data.(type) {
 	case *tlaValueTuple:
 		idx := int(argument.AsNumber())
-		require(idx >= 1 || idx <= data.Len(), "tuple indices must be in range; note that tuples are 1-indexed in TLA+")
+		require(idx >= 1 && idx <= data.Len(), "tuple indices must be in range; note that tuples are 1-indexed in TLA+")
 		return data.Get(idx - 1).(TLAValue)
 	case *tlaValueFunction:
 		value, ok := data.Get(argument)
@@ -371,11 +371,11 @@ func TLA_GreaterThanSymbol(lhs, rhs TLAValue) TLAValue {
 
 func TLA_DotDotSymbol(lhs, rhs TLAValue) TLAValue {
 	from, to := lhs.AsNumber(), rhs.AsNumber()
-	builder := immutable.NewListBuilder()
+	builder := immutable.NewMapBuilder(TLAValueHasher{})
 	for i := from; i <= to; i++ {
-		builder.Append(i)
+		builder.Set(NewTLANumber(i), true)
 	}
-	return TLAValue{&tlaValueTuple{builder.List()}}
+	return TLAValue{&tlaValueSet{builder.Map()}}
 }
 
 func TLA_DivSymbol(lhs, rhs TLAValue) TLAValue {
@@ -909,7 +909,7 @@ func TLA_Tail(v TLAValue) TLAValue {
 func TLA_SubSeq(v, m, n TLAValue) TLAValue {
 	tuple := v.AsTuple()
 	from, to := int(m.AsNumber()), int(n.AsNumber())
-	require(from <= to && from >= 0 && to <= tuple.Len(), "to call SubSeq, from and to indices must be in-bounds")
+	require(from <= to && from >= 1 && to <= tuple.Len(), "to call SubSeq, from and to indices must be in-bounds")
 	return TLAValue{&tlaValueTuple{tuple.Slice(from-1, to)}}
 }
 

distsys/tlaplus_test.go

@@ -33,6 +33,13 @@ func TestTLAModel(t *testing.T) {
 			},
 			ExpectedResult: "[x \\in {} |-> x]",
 		},
+		{
+			Name: "1 .. 3",
+			Operation: func() TLAValue {
+				return TLA_DotDotSymbol(NewTLANumber(1), NewTLANumber(4))
+			},
+			ExpectedResult: "{1, 2, 3, 4}",
+		},
 	}
 
 	for _, test := range tests {

test/files/general/ExprTests.tla.gotests/go.mod

@@ -1,6 +1,6 @@
 module example.org/exprtests
 
-go 1.14
+go 1.13
 
 replace github.com/UBC-NSS/pgo/distsys => ../../../../distsys
 

test/files/general/dqueue.tla.gotests/go.mod

@@ -1,6 +1,6 @@
 module example.org/dqueue
 
-go 1.14
+go 1.13
 
 replace github.com/UBC-NSS/pgo/distsys => ../../../../distsys
 

test/files/general/load_balancer.tla.gotests/go.mod

@@ -1,6 +1,6 @@
 module example.org/load_balancer
 
-go 1.14
+go 1.13
 
 replace github.com/UBC-NSS/pgo/distsys => ../../../../distsys
 

test/files/general/replicated_kv.tla.gotests/go.mod

@@ -1,6 +1,6 @@
 module example.org/replicated_kv
 
-go 1.14
+go 1.13
 
 replace github.com/UBC-NSS/pgo/distsys => ../../../../distsys
 

test/pgo/DistsysTests.scala

@@ -0,0 +1,9 @@
+package pgo
+
+import org.scalatest.funsuite.AnyFunSuite
+
+class DistsysTests extends AnyFunSuite {
+  test("distsys module tests") {
+    os.proc("go", "test").call(cwd = os.pwd / "distsys")
+  }
+}

test/pgo/TLAExpressionFuzzTests.scala

@@ -30,7 +30,7 @@ class TLAExpressionFuzzTests extends AnyFunSuite with ScalaCheckPropertyChecks {
     os.write(modFile,
       s"""module example.org/testbed
          |
-         |go 1.14
+         |go 1.13
          |
          |replace github.com/UBC-NSS/pgo/distsys => ${os.pwd / "distsys"}
          |
@@ -99,6 +99,7 @@ class TLAExpressionFuzzTests extends AnyFunSuite with ScalaCheckPropertyChecks {
               throw err
           }
 
+          os.proc("go", "mod", "tidy").call(cwd = workDir)
           os.proc("go", "mod", "download").call(cwd = workDir)
 
           try {