Designing stabilizing protocols is hard, therefore Protocon exists to automate this task.
It performs a backtracking search to choose actions that finite-state processes should follow in order to converge to a set of legitimate states.
We call this shadow/puppet synthesis, where the legitimate states and behavior can be specified indirectly using shadow variables.
Because the problem is hard, one can leverage multiple cores/nodes for parallel search with OpenMP (via the
-parallel flag) or MPI (via the
The project's main page http://asd.cs.mtu.edu/projects/protocon/ contains executables and short tutorials.
How to Run
make from the top-level directory to build object files in
bld/ and place the resulting executables in
make mkdir tmp ./bin/protocon -x examplespec/ColorRing.prot -o tmp/solution.prot
git clone https://github.com/grencez/protocon.git protocon cd protocon git submodule init git submodule update mkdir -p bld/ext cd bld/ext cmake ../.. make
If you're on a Mac, read on.
Was CMake not found?
If so, make sure it's installed and launch its GUI.
Specify its source directory as
/path/to/protocon/ and the build directory as
Now there should be a makefile in
bld/ext/, so in the terminal type
Besides Qt, all essential dependencies are automatically downloaded when running
- glu 2.4
- Library for multi-valued decision diagrams (MDDs).
- Qt4 4.8
- For the gui.
- Optional logic minimization tool when -espresso flag is used.
- This work was sponsored by the NSF grant CCF-1116546.
- Superior, a high performance computing cluster at Michigan Technological University, was used in obtaining benchmarks and some results.