joshua/nominal-lstar
1
Fork 0
mirror of https://github.com/Jaxan/nominal-lstar.git synced 2025-04-27 22:57:45 +02:00
Code Issues Releases Activity

Updates README accordingly

Browse source
This commit is contained in:
Joshua Moerman 2017-10-21 10:45:23 +02:00
parent 7da6db27b3
commit e91859b61f
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
README.md
View file

@ -103,6 +103,11 @@ equivalence queries through the terminal. The alphabet is fixed in
`Main.hs`, so change it if you need a different alphabet (it should `Main.hs`, so change it if you need a different alphabet (it should
work generically for any alphabet). work generically for any alphabet).
Additionally, one can run the `NominalAngluin2` executable instead,
if provides an easier to parse protocol for membership queries. Hence
it is more suitable for automation. This will first ask for the alphabet
which should be either `ATOMS` or `FIFO`.
A run might look like the following. The lines with `Q:` are queries, A run might look like the following. The lines with `Q:` are queries,
answered by myself on the lines with `A:` or `>`. answered by myself on the lines with `A:` or `>`.
``` ```
@ -139,3 +144,9 @@ A: False
Q: [1,0,1] Q: [1,0,1]
A: A:
``` ```
# Changes since first release
* Better support for interactive communication.
* Optimisation: add only one row/column to fix closedness/consistency