POET (Partial Order Exploration Tools) is a set of state-of-the-art exploration techniques that use partial orders to compactly represent the state space of programs.
Partial order representations are particularly relevant for exploration of concurrent systems, the main motivation of this project.
For stable versions and to reproduce experimental results in research papers please consult POET's wiki
-
Install the Haskell Platform.
Make sure you can run the commands ghc, cabal, and happy. -
Install the simple-c package
-
Install poet: git clone git@github.com:marcelosousa/poet.git cd poet cabal install
This will create the executable poet @ dist/build/poet/
Note that it is likely that master is currently unstable.
There are several available modes:
- poet frontend - prints the result of the front-end
- poet execute - executes the system with a non-deterministic schedule
- poet explore - invokes the explicit-state model checker
For more information, poet --help.
Note: Due to a difference in the Haskell library for command arguments, it may be the case for some operating systems it is required to prefix the input file with -i=.
Also check the repository con-benchmarks for a collection of benchmarks used during the development of POET.
Marcelo Sousa (msousa at cs dot ox dot ac dot uk). University of Oxford, UK.