Merge remote-tracking branch 'origin/master' into unstable

.github/workflows/build.yml

@@ -0,0 +1,53 @@
+name: Testing compiling slugs
+
+on: [push]
+
+env:
+  BUILD_TYPE: Release
+  CCACHE_VERSION: 4.2.1
+
+jobs:
+  build:
+    name: ${{ matrix.config.name }}
+    runs-on: ${{ matrix.config.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        config:
+        - {
+            name: "Ubuntu Latest GCC", 
+            os: ubuntu-latest,
+            cc: "gcc", cxx: "g++"
+          }
+        - {
+            name: "MacOs Latest", 
+            os: macos-latest,
+          }
+
+
+    steps:
+      # SRC: https://stackoverflow.com/questions/67457510/git-submodule-update-remote-merge-yields-fatal-needed-a-single-revision
+    - uses: actions/checkout@main
+      with:
+         # we need the submodules.
+         submodules: recursive
+    - name: Update submodule.
+      run: git submodule update --remote
+    - name: Install various packages needed 
+      run: |
+         if [ "$RUNNER_OS" == "Linux" ]; then
+              sudo apt-get install build-essential libboost-all-dev
+         elif [ "$RUNNER_OS" == "Windows" ]; then
+              # Unsupported as of now.
+              choco install stuff
+         elif [ "$RUNNER_OS" == "macOS" ]; then
+              brew install boost
+         else
+              echo "$RUNNER_OS not supported"
+              exit 1
+         fi
+    - name: Make the slugs executable
+      run: cd src; make
+    - name: Test a simple slugs run
+      run: time src/slugs examples/firefighting.slugsin
+

README.md

@@ -6,10 +6,12 @@ If you want to cite slugs in a scientific paper, please cite its tool paper:
 
 - Rüdiger Ehlers and Vasumathi Raman: _Slugs: Extensible GR(1) Synthesis_. 28th International Conference on Computer Aided Verification (CAV 2016), Volume 2, p.333-339
 
-You can find an author-archived version of the paper [here](http://motesy.cs.uni-bremen.de/pdfs/cav2016.pdf). The paper has an appendix that contains an introduction to using slugs and its input language.
+You can find an author-archived version of the paper [here](https://www.ruediger-ehlers.de/papers/cav2016.pdf). The paper has an appendix that contains an introduction to using slugs and its input language.
 
 The slugs distribution comes with the CUDD library for manipulating binary decision diagrams (BDDs), written by Fabio Somenzi. Please see the README and LICENSE files in the `lib/cudd-3.0.0` folder for details. The _dddmp_ library for loading and saving BDDs that comes with CUDD has other licensing terms than CUDD that permit only academic and educational use. Please consult the source files in the `lib/cudd-3.0.0/dddmp` folder for details.
 
+An introduction video to reactive synthesis with a focus on generalized reactivity(1) synthesis [here](https://www.ruediger-ehlers.de/blog/introtoreactivesynthesis.html). It also contains a Slugs tool demo.
+
 
 Installation
 ============

tools/explicitStrategyToGraphviz.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+#
+# Takes the output of "slugs --explicitStrategy ...other options..." and generates input to GraphViz from it.
+#
+# Pipe the output of slugs to this tool
+import sys
+
+propositions = None
+states = {}
+transitions = {}
+
+for line in sys.stdin.readlines():
+  if line.startswith("State"):
+    assert line.count("<")==1
+
+    # Split line into state/rank number and proposition values
+    linePart1 = line[0:line.index("<")]
+    linePart2 = line[line.index("<"):].strip()
+    linePart1 = linePart1.split(" ")
+    stateNo = linePart1[1]
+    rank = linePart1[4]
+
+    # Parsing proposition values
+    assert linePart2[0]=="<"
+    assert linePart2[-1]==">"
+    linePart2 = [a.strip().split(":") for a in linePart2[1:len(linePart2)-1].split(",")]
+    thesePropositions = [a[0] for a in linePart2]
+    theseValues = [a[1] for a in linePart2]
+
+    if not propositions is None:
+      assert propositions == thesePropositions
+    propositions = thesePropositions
+
+    states[stateNo] = (rank,theseValues)
+  if line.strip().startswith("With successors : "):
+    successors = line.strip()[18:]
+    successors = [a.strip() for a in successors.split(",")]
+    transitions[stateNo] = successors
+
+# Empty output
+if len(states)==0:
+  print("digraph { \"Empty implementation\"; }")
+  sys.exit(0)
+
+# Parsing done. Write
+print("digraph {")
+print("node [shape=tab] \""+",".join(propositions)+"\";")
+
+for (state,(rank,values)) in states.items():
+  print("\""+state+"\" [shape=box,label=\""+"".join(values)+"/"+rank+"\"];")
+for state in states:
+  for b in transitions[state]:
+    print("\""+state+"\" -> \""+str(b)+"\";")    
+print("}")
+
+