add documentation

.github/workflows/docs.yaml

@@ -0,0 +1,52 @@
+name: website
+
+# build the documentation whenever there are new commits on main
+on:
+  push:
+    branches:
+      - dev
+      # Alternative: only build for tags.
+      # tags:
+      #   - '*'
+
+# security: restrict permissions for CI jobs.
+permissions:
+  contents: read
+
+jobs:
+  # Build the documentation and upload the static HTML files as an artifact.
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: mamba-org/setup-micromamba@v1
+        with:
+          environment-file: environment.yaml
+          cache-environment: true
+          post-cleanup: 'all'
+
+      - run: pip install -e .
+        shell: bash -el {0}
+      - run: |
+          pdoc -o docs/docs/ syma '!syma.monitoring'
+          pandoc --standalone -o docs/index.html --metadata title="Symbolic Automata Monitors" README.md
+        shell: bash -el {0}
+
+      - uses: actions/upload-pages-artifact@v2
+        with:
+          path: docs/
+
+  # Deploy the artifact to GitHub pages.
+  # This is a separate job so that only actions/deploy-pages has the necessary permissions.
+  deploy:
+    needs: build
+    runs-on: ubuntu-latest
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - id: deployment
+        uses: actions/deploy-pages@v2

README.md

@@ -11,6 +11,59 @@ This is purely a package that I use in my research, and haven't really documente
 of things, nor does this have a lot of testing. Things mostly work, but open a issue if
 you do find something or send a pull request to fix it.
 
+## Example
+
+![An automaton for the specification "`a` and `b` need to be satisfied before `c`"](examples/specification1.tikz.png) 
+
+The following code creates an automaton `aut` that
+represents the above specification automaton:
+
+```python
+from syma import SymbolicAutomaton
+
+aut = SymbolicAutomaton()
+
+# Symbolic variable declarations
+a = aut.declare_bool("a")
+b = aut.declare_bool("b")
+c = aut.declare_bool("c")
+
+# Location definitions
+aut.add_location(0, initial=True)
+aut.add_location(1)
+aut.add_location(2)
+aut.add_location(3)
+aut.add_location(4, accepting=True)
+
+# Transition definitions
+# q0
+aut.add_transition(0, 0, guard=(~a & ~b))
+aut.add_transition(0, 1, guard=(a & ~b))
+aut.add_transition(0, 2, guard=(~a & b))
+aut.add_transition(0, 3, guard=(a & b & ~c))
+aut.add_transition(0, 4, guard=(a & b & c))
+# q1
+aut.add_transition(1, 1, guard=(~b))
+aut.add_transition(1, 3, guard=(b & ~c))
+aut.add_transition(1, 4, guard=(b & c))
+# q2
+aut.add_transition(2, 2, guard=(~a))
+aut.add_transition(2, 3, guard=(a & ~c))
+aut.add_transition(2, 4, guard=(a & c))
+# q3
+aut.add_transition(3, 3, guard=(~c))
+aut.add_transition(3, 4, guard=c)
+# q4
+aut.add_transition(4, 4, guard=True)
+```
+
+Now, `aut` can be used to check if constraints are satisfied by some input word.
+For more information, check out the documentation for [`SymbolicAutomata`][doc-symaut]
+and [`Constraint`][doc-constraint].
+
+[doc-symaut]: https://anand-bala.github.io/symbolic-automata-monitors/docs/syma.html#SymbolicAutomaton
+[doc-constraint]: https://anand-bala.github.io/symbolic-automata-monitors/docs/syma.html#Constraint
+
 ## References
 
 - S. Jakšić, E. Bartocci, R. Grosu, and D. Ničković, “An Algebraic Framework for Runtime

environment.yaml

@@ -7,7 +7,9 @@ dependencies:
   - scipy~=1.7
   - matplotlib~=3.4
   - spot~=2.10
+  - pandoc
   - pip
   - pip:
-    - z3-solver~=4.8
-    - networkx~=2.6
+      - z3-solver~=4.8
+      - networkx~=2.6
+      - pdoc