gmc-synthesis /

Filename Size Date modified Message
hknt-1.0
tests
1.4 KB
1.4 KB
1.4 KB
1.5 KB
10.1 KB
1.8 KB
7.1 KB
4.8 KB
5.0 KB
11.6 KB
1.8 KB
2.1 KB
901 B
3.9 KB
7.9 KB
1.1 KB
2.8 KB
3.5 KB
17.1 KB
1.4 KB
1.4 KB
12.1 KB
4.2 KB
4.3 KB
2.9 KB
693 B
364 B
405 B
This tool implements the theory introduced in **From Communicating Machines to Graphical Choreographies** by Julien Lange,  Emilio Tuosto, and Nobuko Yoshida.

See http://www.doc.ic.ac.uk/~jlange/demo.tar.gz for sample of graphical outputs; all the systems in this archive are GMC.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

# Required Tools/ Libraries #
The following tools and libraries are required.

* graphviz (and python-numpy if you would like to run the benchmarks scripts)

You can install via the command "sudo apt-get install graphviz" on
ubuntu/debian

- Haskell platform (cf. http://www.haskell.org/platform/)

- MissingH (a Haskell libraries)
  You can install it via the command:
```
#!

cabal install MissingH split Graphalyze
```


- HKC (slight variation on git) --
  http://perso.ens-lyon.fr/damien.pous/hknt/
  To compile: the modified version, use the following commands:
     - cd hknt-1.0/
     - make
     (you will need OCaml, ./hknt-1.0/README)

- Petrify -- http://www.lsi.upc.edu/~jordicf/petrify/

NB: The tool has been tested on Ubuntu 13.04 and Mac OS X (v10.9)


# Compilation #
To compile the tool, run the following command:

```
#!

 ghc -threaded --make GMC.hs && ghc --make BuildGlobal.hs
```


# Configuration #
To configure the tool to you environment, edit the file "rungmc.py" so
that the PETRY variable is set to the binary of petrify, e.g., PETRY =
"/home/myuser/mysoftware/petrify/bin/petrify"


# Syntax of the input files #
The syntax of the input files is similar to that of petrify, for
instance,
```
#!

.outputs
.state graph
q0 1 ! hello q1
q0 1 ! bye q1
.marking q0
.end

.outputs 
.state graph
q0 0 ? hello q1
q0 0 ? bye q1
.marking q0
.end
```
specifies a system of two machines, machine 0, may send either "hello"
or "bye" to machine 1, which is ready to receive either "hello" or
"bye" from machine 0.


# Running the tool #
You can run the tool via the command: ./rungmc <path/to/cfsms>



# Getting the results #
If the system in <cfsms> is GMC only of the tool ouputs the following
two lines:
```
#!

<<----- Partial GMC Check: +++True+++ ----->> 
Is the system Language-equivalence Representable (part (i))? ^^^True^^^
```



If <cfsms> is GMC, then the "outputs" folder contains the following files:

* <cfsms>_a_machines.svg : a graphical representation of <cfsms>
* <cfsms>_c_global.svg : a graphical representation of the global graph synthesised from <cfsms>

and, if "debug = True" in rungmc.py, 

* <cfsms>_b_ts.svg : a graphical representation of TS(<cfsms>)
* <cfsms>_finalpn.svg : a reprensation of the Petri net to be transformed into the pre-global graph
* <cfsms>_preglobal.svg : the pre-global graph