Add a small example for use in a tutorial (#38)

Co-authored-by: Gabriela Moreira <gabrielamoreiramafra@gmail.com>
Co-authored-by: Thomas Pani <thomas.pani@gmail.com>

* Make actions parameterized

Following guidance from @Kukovec on best practices in structuring action
data dependencies and explanation of the advantages of prenex form.

Makefile

@@ -61,7 +61,7 @@ lint:
 	poetry run black . --check
 
 test:
-	poetry run pyright chai/ tests/ integration-tests/
+	poetry run pyright chai/ tests/ integration-tests/ example/
 	poetry run pytest -s tests/
 
 integration:

README.md

@@ -25,6 +25,7 @@ poetry add git+https://github.com/informalsystems/apalache-chai.git
 ## Documentation
 
 - [API Documentation](https://informalsystems.github.io/apalache-chai/chai.html)
+- [Example Application](./example/README.md)
 
 ## Development
 

example/FileSystem.tla

@@ -0,0 +1,137 @@
+------------------- MODULE FileSystem -----------------------
+\* A small example spec of some file system operations.
+\* This spec is meant for use in the `app.py` in the same directory,
+\* which demonstrates use of the chai client for interacting with
+\* the Apalache server.
+
+EXTENDS Apalache, Variants, Sequences, Integers, FiniteSets
+
+
+\*********\
+\* STATE *\
+\*********\
+
+CONSTANT
+    \* The names that can be used as path segments.
+    \* @type: Set(Str);
+    Names
+
+VARIABLES
+    \* The set of all files in the system.
+    \* @type: Set($file);
+    files,
+    \* The command issued.
+    \* @type: $cmd;
+    cmd
+
+
+\**********\
+\* DOMAIN *\
+\**********\
+
+\** Representation of files, identified by their kind and their path.
+\*
+\* @typeAlias: path = Seq(Str);
+\* @typeAlias: file = File($path) | Dir($path);
+\* @type: $path => $file;
+File(path) == Variant("File", path)
+\* @type: $path => $file;
+Dir(path) == Variant("Dir", path)
+
+IsDir(f) == "Dir" = VariantTag(f)
+IsFile(f) == "File" = VariantTag(f)
+
+\* @type: $file => $path;
+FilePath(f) == VariantGetOrElse("Dir", f, VariantGetUnsafe("File", f))
+
+\* @type: (Seq(a), Seq(a)) => Bool;
+IsPrefix(prefix, s) ==
+  /\ Len(s) >= Len(prefix)
+  /\ \A i \in DOMAIN prefix: prefix[i] = s[i]
+
+\** The children of a file (i.e., the contents of a directory)
+\*
+\* NOTE: The `Children` relation is reflexive: each file is its own child.
+\*
+\* @type: $file => Set($file);
+Children(p) ==
+  { child \in files: IsPrefix(FilePath(p), FilePath(child)) }
+
+\* @type: Seq($file);
+NoFile == <<>>
+
+\** Representation of commands that operate on the file system.
+\*
+\* A $cmd is a triple holding:
+\*
+\* - the command name
+\* - the path(s) it operates on
+\* - the command's output (if any)
+\*
+\* @typeAlias: cmd = << Str, Seq($file), Set($file) >> ;
+\* @type: $file => $cmd;
+TouchCmd(p) == << "Touch", <<p>>, {} >>
+\* @type: $file => $cmd;
+MkDirCmd(p) == << "MkDir", <<p>>, {} >>
+\* @type: $file => $cmd;
+LsCmd(p)    == << "Ls", <<p>>, Children(p) >>
+\* @type: () => $cmd;
+None == << "None", NoFile, {} >>
+
+
+\***********\
+\* ACTIONS *\
+\***********\
+
+\* @type: ($file, Str) => Bool;
+Touch(dir, name) ==
+  LET newFile == File(Append(FilePath(dir), name)) IN
+  /\ files' = { newFile } \union files
+  /\ cmd' = TouchCmd(newFile)
+
+
+\* @type: ($file, Str) => Bool;
+MkDir(dir, name) ==
+  LET newDir == Dir(Append(FilePath(dir), name)) IN
+  /\ files' = { newDir } \union files
+  /\ cmd' = MkDirCmd(newDir)
+
+\* @type: $file => Bool;
+Ls(p) ==
+  /\ cmd' = LsCmd(p)
+  /\ UNCHANGED files
+
+Next ==
+  \E f \in files:
+    \/ /\ IsDir(f)
+      /\ \E n \in Names:
+        \/ Touch(f, n)
+        \/ MkDir(f, n)
+    \/ Ls(f)
+
+
+\******************\
+\* INITIALIZATION *\
+\******************\
+
+CInit == Names = {"foo", "bar", "baz"}
+
+Init ==
+  /\ files = { Dir(<<"/">>) }
+  /\ cmd = None
+
+
+\**************\
+\* INVARIANTS *\
+\**************\
+
+MinPathLength == 5
+MinDirSize == 5
+
+Inv ==
+  ~ /\ \E p \in files: Len(FilePath(p)) > MinPathLength
+    /\ Cardinality(cmd[3]) > MinDirSize
+
+\* @type: << Set($file), $cmd >>;
+View == << files, cmd >>
+============================================================

example/README.md

@@ -0,0 +1,68 @@
+# Chai Example Application
+
+This directory contains a demo showing how the `apalache-chai` client libray can be
+used to interact with the Apalache server.
+
+The demo is defined in [./app.py](./app.py). It performs the following actions:
+
+- Connects to a running Apalache server
+- Makes an RPC call to the server to parse a TLA+ file into a JSON representation
+  of the model
+- Updates the model to add some values taken from CLI args
+- Makes an RPC call to the server to obtain counter-examples from the
+  model-checker
+- Produce a (crappy) graph showing the state transitions in the counter-examples
+
+The spec used to generate counterexamples is defined in
+[./FileSystem.tla](./FileSystem.tla). It specifies a simple filesystem
+supporting three actions:
+
+- Creating flat files (like `touch`)
+- Creating directories (like `mkdir`)
+- Listing the children of a directory  (like `ls`)
+
+The spec is used to generate counter-examples leading up to certain states. The
+python app takes CLI parameters that determine the properties of the states, and
+does plumbing to interact with the Apalache server.
+
+Here's an example of a session:
+
+```sh
+$  poetry run python example/app.py --help
+usage: app.py [-h] [--names NAMES] [--path-length PATH_LENGTH] [--dir-size DIR_SIZE] [--branches BRANCHES]
+
+optional arguments:
+  -h, --help            show this help message and exit
+  --names NAMES         which names can be used for forming file paths
+  --path-length PATH_LENGTH
+                        the system must include a path with at least this many components
+  --dir-size DIR_SIZE   A directory with at least this many children must exist
+  --branches BRANCHES   the max paths to a suitable state that should be found
+
+# Start the apalache server in the background
+$ apalache-mc server > /dev/null &
+
+# Run the program, and generate the state graph
+$  poetry run python example/app.py --names foo,bar,baz,qux --path-length 4 --branches 5
+Connection to the Apalache server established
+Source file loaded from /home/sf/Sync/informal-systems/apalache/apalache-chai/example/FileSystem.tla
+Model parsed, typechecked, and loaded
+Model parameters updated from CLI params
+Counter examples have been obtained
+The state graph has been saved to demo-states-graph.png
+
+# Foreground apalache and kill it
+$  fg
+apalache-mc server > /dev/null
+^C
+```
+
+The resulting graph will look something like this:
+
+![Example of state graph](./demo-states-graph.png)
+
+The labels on the edges show the command that transitions between each state.
+The label on the nodes show the indexes of that state in the form
+`(trace_n,state_n)` where `trace_n` is the number of the counter-example trace
+in which the state was procued and `state_n` is the index of state in that
+trace. These can be cross referenced against the counter example data.