This document explains how to use Spot with GreatSPN. Please correct mistakes and complete holes.

1. Installation

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

GetSpot or any SpotSnapshot.

Configure Spot with

% ./configure --prefix=DIR1 --with-gspn=DIR2

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

% make

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.

If you have also installed FrameKit, your model will be generated on your FrameKit server machine, in your WorkSpace directory,

${WorkSpace}/AMI-Net/mymodel/FK_MNGR/.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 :

Export the model to GreatSPN .net/.def format using Snow.

From Macao, simply invoke the GreatSPN tools. Model will be generated in

${WorkSpace}/AMI-Net/mymodel/FK_MNGR/nets/model.{def,net}

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

Notes:

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:

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.

Example:

./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.)

SpotGspnHowTo (last edited 2004-06-29 16:48:19 by diane)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.