This document explains how to use Spot with GreatSPN. Please correct mistakes and complete holes.
1.1. Getting and Building GreatSPN
Latest GreatSPN versions are stored on a CVS in Torino. We have yet to setup a local checkout that is rebuilt nightly. By the meantime, I'm using the version that is in /data/adl/greatspn/ on framekit-dev.
Unless your version is already built, all you have to do is
% cd SOURCES % make -f Makefile.Linux-OpenMotif
GreatSPN assumes Berkeley Yacc. So if you yacc is a link to GNU Bison and Berkeley Yacc is installed as byacc, you will want to edit Makefile.Linux-OpenMotif and set
YACC = byacc
Compilation is likely to display many errors and can even fail before the end. That may be OK or not. Checkout whether the libraries have been built with
% ls ../i686_R2.6.3-4mdk/2bin/lib libgspnRG.a libgspnSRG.a libgspnSSP.a
(The i686_R2.6.3-4mdk part may be different for you.)
1.2. Getting and Building Spot
Configure Spot with
% ./configure --prefix=DIR1 --with-gspn=DIR2
DIR1 is the directory where the library and its header will be installed. It default to /usr/local/. (AFAIC, I always install packages on my account with --prefix ~/usr/`arch`.)
DIR2 is the root of GreatSPN's source tree. (For instance it's /data/adl/greatspn in my case.)
During configure's execution, you should see the following lines.
checking for /data/adl/greatspn/SOURCES/contrib/version.sh... yes checking for initialize in -lgspnRG... yes checking for initialize in -lgspnSRG... yes checking for initialize in -lgspnSSP... yes
Build Spot with
Finally install it with
% make install
Presently this last step is not necessary, because the binaries we are going to use for these experiments are those used in Spot's test suite. They are not meant to be installed since they have very horrible interfaces.
2. Using Snow (for RG or SRG)
2.1. Drawing a model with Macao
As Macao is currently only MacOS compatible, you need to find a Mac. These are the colorful thingies with an apple logo.
You then can draw your model with Macao, using the AMI-Net formalism. This produces a CAMI syntax description of your model.
Although this is optional, I recommend you syntax check your model.
The Matrice/Sandrine duo does not treat immediate transitions.
Otherwise, you can select your whole model (apple-a) in Macao and copy-paste it to a plain text file, this will also produce a CAMI file.
2.2. Specifying your LTL formula and Atomic properties
You now need to define the property you wish to check on your model.
2.2.1. Using Observation Transitions for Atomic Properties
An observation transition is like a transition of your model, except it is never actually fired. It is used to observe some behavior of your system, hence its name.
The atomic property defined by an observation transition is considered TRUE in any state of the model in which it is enabled.
You may use both pre and inhibitor arcs in your definition of an observation transition, but not post arcs, as it will not be fired anyway. Guards are also allowed on observation transitions.
You may define as many observation transitions as you wish, only those that are used in the LTL formula to be checked will be taken into account at state-space generation time.
There are currently two ways of defining observation transitions :
Directly from your model editor (Macao or GreatSPN). A transition with name starting by PROP_ is considered to be an observation transition and is treated accordingly.
Create a text file in which you define your observation transitions in a straightforward textual format. See page TobsFormat for a description of this text format. Pass this file as the "-p" (for properties) option to Snow.
Export the model to GreatSPN .net/.def format using Snow.
From Macao, simply invoke the GreatSPN tools. Model will be generated in
I think all you need is to use one of the menu entries ending with RG or SRG, and the .net/.def files will appear in the depths of the FrameKit workspace.
This export can fail badly on syntax errors (hence the previous step).
2.3. Preparing the model for GreatSPN
Once you've got the .net/.def files, you have to process them through the trans2prop.pl script. There is one version in ~adl/data/work/trans2prop.pl, but I know Yann and Soheib have an improved one so it could read net drawn using the drawing tool of GreatSPN.
If you have toto.net and toto.def, the process should look as follows.
% ls toto.* toto.def toto.net % trans2prop.pl toto % mv toto.nettmp toto.net % ls toto.* toto.def toto.net toto.tobs
Do not forget this mv.
The resulting toto.tobs contains all the observing transitions that have been extracted from toto.net.
2.4. Model-checking with Spot
Go back into Spot's source tree, and visit the iface/gspn/ directory. Amongst other things, this directory should contain two programs named ltlgspn-rg and ltlgspn-srg. These two programs can be used identically, only the GreatSPN implementation changes. They should display their usage when run without argument.
If your toto model contains two observing transitions PROP_FOO and PROP_BAR, you can verify the LtlFormula FOO U BAR with
% ./ltlgspn-srg -e -f '!("FOO" U BAR)' FOO BAR
F is an LTL operator, so FOO needs double-quotes so that Spot does not interpret it as F(OO). (See LtlSyntax for details.)
- in this interface it's the user's job to negate the formula to verify
(hence the leading ! operator).
Let me stress that these are test programs for Spot and should not be used in FrameKit as-is. (In fact these are scripts that run some hidden binaries in a way they can use the Spot library even though it is not installed. That's why you cannot move them.) Decent user utilities with an interface suitable to FrameKit have yet to be done, and once that is done they will be installed by make install.
3. Using Soheib's work (SSP)
You should prepare the following elements:
a toto.def/toto.net pair for the symmetric par of the model
a control automaton toto.con with the asymmetries
a file defining the atomic properties toto.prop
Ask Soheib for details. I've stored one of his example in ~adl/data/ex-soheib-ssp/.
In Spot's iface/gspn/ you can use ./ltlgspn-ssp like the two other, except you must additionally specify the control automaton. ./ltlgspn-ssp also allow three emptiness-check variants corresponding to Soheib's works on inclusion checking.
./ltlgspn-ssp -c -e2 -f ~adl/data/ex-soheib-ssp/WCSsym \ 'AT2 U ID2' ~adl/data/ex-soheib-ssp/WCSsym.con AT2 ID2
Beware that the -c option (which computes a counter-example instead of a empty/non-empty answer) can be very expensive because it enumerate all the paths in a strongly connected component. (This is true for ltlgspn-rg and ltlgspn-srg as well.)