Skip to content
GitLab
Commit 2d1460a2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Kill the gspn-ssp benchmark (it was not working anymore). 

* bench/gspn-ssp/: Delete recursively.
* bench/Makefile.am, README, configure.ac: Adjust.
parent 649e8e2d
Expand all Hide whitespace changes
Inline Side-by-side
README
View file @ 2d1460a2
......@@ -151,7 +151,6 @@ doc/ Documentation for libspot.
spot.html/ HTML reference manual for the library.
bench/ Benchmarks for ...
emptchk/ ... emptiness-check algorithms,
gspn-ssp/ ... various symmetry-based methods with GreatSPN,
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
ltlcounter/ ... translation of a class of LTL formulae,
ltlclasses/ ... translation of more classes of LTL formulae,
......
bench/Makefile.am
View file @ 2d1460a2
## Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
## Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
......@@ -21,5 +21,5 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product ltlcounter \
SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \
ltlclasses wdba
bench/gspn-ssp/Makefile.am deleted 100644 → 0
View file @ 649e8e2d
## Copyright (C) 2008 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
## Spot is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published by
## the Free Software Foundation; either version 2 of the License, or
## (at your option) any later version.
##
## Spot is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
## License for more details.
##
## You should have received a copy of the GNU General Public License
## along with Spot; see the file COPYING. If not, write to the Free
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
TEMPLATES =
MODELS =
include modelgen.mk
include bench.mk
EXTRA_DIST = \
$(TEMPLATES) \
templates/common \
templates/gen \
README
run_bench = tools/runbench
dist_noinst_SCRIPTS = \
tools/bench-create \
tools/trans2prop.pl \
tools/sum \
$(run_bench)
$(RESULTS): defs
nodist_check_DATA = $(RESULTS)
clean-local:
rm -rf models results
bench/gspn-ssp/README deleted 100644 → 0
View file @ 649e8e2d
This directory contains an evolution of the benchmark we used in
the following papers.
* Souheib Baarir and Alexandre Duret-Lutz. Test de vacuité pour
automates de Büchi ensemblistes avec tests d'inclusion. In Actes du
6e Colloque Francophone sur la Modélisation des Systèmes Réactifs
(MSR'07), pages 19-34. Hermes-Lavoisier, October 2007.
* Souheib Baarir and Alexandre Duret-Lutz. Emptiness check of powerset
Büchi automata. In Proceedings of the 7th International Conference
on Application of Concurrency to System Design (ACSD'07), pages
41-50. IEEE Computer Society, July 2007.
* Souheib Baarir and Alexandre Duret-Lutz. Emptiness check of powerset
Büchi automata. Technical report 2006/003, Université Pierre et
Marie Curie, LIP6-CNRS, Paris, France, October 2006.
It is unlikely that you will be able to run this benchmark unless you
are close to Souheib et Alexandre, because of it requires
(1) a customized version of GreatSPN that has never been released,
(2) a tool called Snow that has never been released either
(see http://spot.lip6.fr/wiki/Snow)
Here is some documentation nonetheless.
Layout
======
template/
This directory contains the original models. Some of them
are parametrized and need to be instantiated.
WCSsym/
A parameterized model for a critical section in which
processes are assigned a different priority (yielding an
asymmetry). The parameter is the number of processes.
bagrodia/
A parameterized model of Rajive L Bagrodia's distributed
rendez-vous algorithm. The parameter is the number of
processes.
predef/
Some preinstanciated models for WCS that do not use
symmetries.
models/
This directory is built by make and will contain the actual
instances of each model.
results/
This directory will be built by make and will contain the result of
each test.
tools/
Scripts used by the benchmark.
tools/modelgen-create
is a script that creates , the makefile rules for instantiating
the models in the models/ directory.
tools/bench-create
is a script that creates modelgen.mk and bench.mk.
modelgen.mk contains the rules for instantiating
the models in the models/ directory, and bench.mk
those for putting the results in the results/ directory.
Unless you add new models you should not need to run this,
because the Makefiles are distributed with Spot.
tools/sum
(for summary) is the script that should be run to display the
results of the benchmark. This script can be run at any point
during the benchmark, and will display the available results.
tools/runbench
is an auxiliary script used in the makefile rules of bench.mk.
Its job is to actually run the ltlgspn-* binaries from iface/gspn/
with the right options. Runbench will also clone the model in a
temporary directory before running any tool : this is because
GreatSPN use many temporary files and we want to be able to run
several test in parallel.
tools/trans2prop.pl
is an auxiliary script used by tools/runbench. It is used in
conjunction with Snow (see link above) to express atomic properties
as transitions in a model.
Running
=======
1) Compile GreatSPN. You should have the following three libraries:
% ls greatspn/i686_R2.6.25.10/2bin/lib
libgspnRG.a libgspnSRG.a libgspnSSP.a
2) Compile Spot using GreatSPN. I use the following command:
% ./configure --with-gspn=GREATSPN_PATH --disable-static LDFLAGS=-lglib-2.0
You should have the following tree binaries :
iface/gspn/ltlgspn-rg
iface/gspn/ltlgspn-srg
iface/gspn/ltlgspn-ssp*
3) Edit bench/gspn-ssp/defs and fix the location of Snow.
4) Go into bench/gspn-ssp/, run "make check" or "make -j2 check" (or more)
if you have several CPUs.
5) Run tools/sum to get a summary of the results. You can run this
even before the above "make check" has finished, but of course this
will only summarize the available results.
What is tested
==============
Each model is tested using differents emptiness check strategies
(these are the ltlgspn-ssp options -e4, -e5, -e6 etc.) against 50
formulaes. Each test (1 model, 1 set of option, 1 formula) produce
one ".log" file in the results/ directory. The tools/sum script
processes all these log files and show how one model with one set of
option averages on the 50 formulae.
bench/gspn-ssp/bench.mk deleted 100644 → 0
View file @ 649e8e2d
This diff is collapsed.
bench/gspn-ssp/defs.in deleted 100644 → 0
View file @ 649e8e2d
# -*- shell-script -*-
# Copyright (C) 2008 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
# Ensure we are running from the right directory.
test -f ./defs || {
echo "defs: not found in current directory" 1>&2
exit 1
}
srcdir='@srcdir@'
# Ensure $srcdir is set correctly.
test -f "$srcdir/defs.in" || {
echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
exit 1
}
RANDLTL='@abs_top_builddir@/src/ltltest/randltl'
LTLGSPNSSP='@abs_top_builddir@/iface/gspn/ltlgspn-ssp'
LTLGSPNSRG='@abs_top_builddir@/iface/gspn/ltlgspn-srg'
SNOW=/home/adl/projs/src/gspn/snow
TRANS2PL='@abs_srcdir@/tools/trans2prop.pl'
TIME='/usr/bin/time -p'
TMPDIR=${TMPDIR-/tmp}
export RANDLTL LTLGSPNSSP LTLGSPNSRG TIME SNOW TRANS2PL TMPDIR
bench/gspn-ssp/modelgen.mk deleted 100644 → 0
View file @ 649e8e2d
# This file is automatically generated by modelgen-create, do not edit.
TEMPLATES += templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop templates/WCSsym/gen
MODELS += models/WCSsym3/stamp
models/WCSsym3/stamp: templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop
mkdir -p 'models/WCSsym3'
cp '$(srcdir)/templates/WCSsym/WCSsym.con' models/WCSsym3/WCSsym3.con
cp '$(srcdir)/templates/WCSsym/WCSsym.net' models/WCSsym3/WCSsym3.net
cp '$(srcdir)/templates/WCSsym/WCSsym.prop' models/WCSsym3/WCSsym3.prop
cp '$(srcdir)/templates/WCSsym/WCSsym.gd' models/WCSsym3/WCSsym3.gd
sed 's/@PR@/pr1,pr2,pr3/' '$(srcdir)/templates/WCSsym/WCSsym.def' > 'models/WCSsym3/WCSsym3.def'
sed 's/:.*//' '$(srcdir)/templates/WCSsym/WCSsym.prop' | tr '\n' ' ' > 'models/WCSsym3/WCSsym3.ap'
touch $@
TEMPLATES += templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop templates/WCSsym/gen
MODELS += models/WCSsym4/stamp
models/WCSsym4/stamp: templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop
mkdir -p 'models/WCSsym4'
cp '$(srcdir)/templates/WCSsym/WCSsym.con' models/WCSsym4/WCSsym4.con
cp '$(srcdir)/templates/WCSsym/WCSsym.net' models/WCSsym4/WCSsym4.net
cp '$(srcdir)/templates/WCSsym/WCSsym.prop' models/WCSsym4/WCSsym4.prop
cp '$(srcdir)/templates/WCSsym/WCSsym.gd' models/WCSsym4/WCSsym4.gd
sed 's/@PR@/pr1,pr2,pr3,pr4/' '$(srcdir)/templates/WCSsym/WCSsym.def' > 'models/WCSsym4/WCSsym4.def'
sed 's/:.*//' '$(srcdir)/templates/WCSsym/WCSsym.prop' | tr '\n' ' ' > 'models/WCSsym4/WCSsym4.ap'
touch $@
TEMPLATES += templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop templates/WCSsym/gen
MODELS += models/WCSsym5/stamp
models/WCSsym5/stamp: templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop
mkdir -p 'models/WCSsym5'
cp '$(srcdir)/templates/WCSsym/WCSsym.con' models/WCSsym5/WCSsym5.con
cp '$(srcdir)/templates/WCSsym/WCSsym.net' models/WCSsym5/WCSsym5.net
cp '$(srcdir)/templates/WCSsym/WCSsym.prop' models/WCSsym5/WCSsym5.prop
cp '$(srcdir)/templates/WCSsym/WCSsym.gd' models/WCSsym5/WCSsym5.gd
sed 's/@PR@/pr1,pr2,pr3,pr4,pr5/' '$(srcdir)/templates/WCSsym/WCSsym.def' > 'models/WCSsym5/WCSsym5.def'
sed 's/:.*//' '$(srcdir)/templates/WCSsym/WCSsym.prop' | tr '\n' ' ' > 'models/WCSsym5/WCSsym5.ap'
touch $@
TEMPLATES += templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop templates/WCSsym/gen
MODELS += models/WCSsym6/stamp
models/WCSsym6/stamp: templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop
mkdir -p 'models/WCSsym6'
cp '$(srcdir)/templates/WCSsym/WCSsym.con' models/WCSsym6/WCSsym6.con
cp '$(srcdir)/templates/WCSsym/WCSsym.net' models/WCSsym6/WCSsym6.net
cp '$(srcdir)/templates/WCSsym/WCSsym.prop' models/WCSsym6/WCSsym6.prop
cp '$(srcdir)/templates/WCSsym/WCSsym.gd' models/WCSsym6/WCSsym6.gd
sed 's/@PR@/pr1,pr2,pr3,pr4,pr5,pr6/' '$(srcdir)/templates/WCSsym/WCSsym.def' > 'models/WCSsym6/WCSsym6.def'
sed 's/:.*//' '$(srcdir)/templates/WCSsym/WCSsym.prop' | tr '\n' ' ' > 'models/WCSsym6/WCSsym6.ap'
touch $@
TEMPLATES += templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop templates/WCSsym/gen
MODELS += models/WCSsym8/stamp
models/WCSsym8/stamp: templates/WCSsym/WCSsym.con templates/WCSsym/WCSsym.net templates/WCSsym/WCSsym.prop templates/WCSsym/WCSsym.gd templates/WCSsym/WCSsym.def templates/WCSsym/WCSsym.prop
mkdir -p 'models/WCSsym8'
cp '$(srcdir)/templates/WCSsym/WCSsym.con' models/WCSsym8/WCSsym8.con
cp '$(srcdir)/templates/WCSsym/WCSsym.net' models/WCSsym8/WCSsym8.net
cp '$(srcdir)/templates/WCSsym/WCSsym.prop' models/WCSsym8/WCSsym8.prop
cp '$(srcdir)/templates/WCSsym/WCSsym.gd' models/WCSsym8/WCSsym8.gd
sed 's/@PR@/pr1,pr2,pr3,pr4,pr5,pr6,pr7,pr8/' '$(srcdir)/templates/WCSsym/WCSsym.def' > 'models/WCSsym8/WCSsym8.def'
sed 's/:.*//' '$(srcdir)/templates/WCSsym/WCSsym.prop' | tr '\n' ' ' > 'models/WCSsym8/WCSsym8.ap'
touch $@
TEMPLATES += templates/bagrodia/bagrodia.con templates/bagrodia/bagrodia.net templates/bagrodia/bagrodia.prop templates/bagrodia/bagrodia.gd templates/bagrodia/bagrodia.def templates/bagrodia/bagrodia.prop templates/bagrodia/gen
MODELS += models/bagrodia2/stamp
models/bagrodia2/stamp: templates/bagrodia/bagrodia.con templates/bagrodia/bagrodia.net templates/bagrodia/bagrodia.prop templates/bagrodia/bagrodia.gd templates/bagrodia/bagrodia.def templates/bagrodia/bagrodia.prop
mkdir -p 'models/bagrodia2'
cp '$(srcdir)/templates/bagrodia/bagrodia.con' models/bagrodia2/bagrodia2.con
cp '$(srcdir)/templates/bagrodia/bagrodia.net' models/bagrodia2/bagrodia2.net
cp '$(srcdir)/templates/bagrodia/bagrodia.prop' models/bagrodia2/bagrodia2.prop
cp '$(srcdir)/templates/bagrodia/bagrodia.gd' models/bagrodia2/bagrodia2.gd
sed 's/@X@/x1,x2/' '$(srcdir)/templates/bagrodia/bagrodia.def' > 'models/bagrodia2/bagrodia2.def'
sed 's/:.*//' '$(srcdir)/templates/bagrodia/bagrodia.prop' | tr '\n' ' ' > 'models/bagrodia2/bagrodia2.ap'
touch $@
MODELS += models/WCSasym3.rg/stamp
models/WCSasym3.rg/stamp: templates/predef/WCSasym3.def templates/predef/WCSasym3.net templates/predef/WCSasym3.tobs
mkdir -p models/WCSasym3.rg
cp '$(srcdir)/templates/predef/WCSasym3.def' 'models/WCSasym3.rg/WCSasym3.rg.def'
cp '$(srcdir)/templates/predef/WCSasym3.net' 'models/WCSasym3.rg/WCSasym3.rg.net'
cp '$(srcdir)/templates/predef/WCSasym3.tobs' 'models/WCSasym3.rg/WCSasym3.rg.tobs'
echo 'P1 P2 P3 P4 P5 P6 P7 P8' > models/WCSasym3.rg/WCSasym3.rg.ap
touch $@
MODELS += models/WCSasym4.rg/stamp
models/WCSasym4.rg/stamp: templates/predef/WCSasym4.def templates/predef/WCSasym4.net templates/predef/WCSasym4.tobs
mkdir -p models/WCSasym4.rg
cp '$(srcdir)/templates/predef/WCSasym4.def' 'models/WCSasym4.rg/WCSasym4.rg.def'
cp '$(srcdir)/templates/predef/WCSasym4.net' 'models/WCSasym4.rg/WCSasym4.rg.net'
cp '$(srcdir)/templates/predef/WCSasym4.tobs' 'models/WCSasym4.rg/WCSasym4.rg.tobs'
echo 'P1 P2 P3 P4 P5 P6 P7 P8' > models/WCSasym4.rg/WCSasym4.rg.ap
touch $@
MODELS += models/WCSasym5.rg/stamp
models/WCSasym5.rg/stamp: templates/predef/WCSasym5.def templates/predef/WCSasym5.net templates/predef/WCSasym5.tobs
mkdir -p models/WCSasym5.rg
cp '$(srcdir)/templates/predef/WCSasym5.def' 'models/WCSasym5.rg/WCSasym5.rg.def'
cp '$(srcdir)/templates/predef/WCSasym5.net' 'models/WCSasym5.rg/WCSasym5.rg.net'
cp '$(srcdir)/templates/predef/WCSasym5.tobs' 'models/WCSasym5.rg/WCSasym5.rg.tobs'
echo 'P1 P2 P3 P4 P5 P6 P7 P8' > models/WCSasym5.rg/WCSasym5.rg.ap
touch $@
MODELS += models/WCSasym6.rg/stamp
models/WCSasym6.rg/stamp: templates/predef/WCSasym6.def templates/predef/WCSasym6.net templates/predef/WCSasym6.tobs
mkdir -p models/WCSasym6.rg
cp '$(srcdir)/templates/predef/WCSasym6.def' 'models/WCSasym6.rg/WCSasym6.rg.def'
cp '$(srcdir)/templates/predef/WCSasym6.net' 'models/WCSasym6.rg/WCSasym6.rg.net'
cp '$(srcdir)/templates/predef/WCSasym6.tobs' 'models/WCSasym6.rg/WCSasym6.rg.tobs'
echo 'P1 P2 P3 P4 P5 P6 P7 P8' > models/WCSasym6.rg/WCSasym6.rg.ap
touch $@
MODELS += models/WCSasym8.rg/stamp
models/WCSasym8.rg/stamp: templates/predef/WCSasym8.def templates/predef/WCSasym8.net templates/predef/WCSasym8.tobs
mkdir -p models/WCSasym8.rg
cp '$(srcdir)/templates/predef/WCSasym8.def' 'models/WCSasym8.rg/WCSasym8.rg.def'
cp '$(srcdir)/templates/predef/WCSasym8.net' 'models/WCSasym8.rg/WCSasym8.rg.net'
cp '$(srcdir)/templates/predef/WCSasym8.tobs' 'models/WCSasym8.rg/WCSasym8.rg.tobs'
echo 'P1 P2 P3 P4 P5 P6 P7 P8' > models/WCSasym8.rg/WCSasym8.rg.ap
touch $@
TEMPLATES += templates/predef/WCSasym3.def templates/predef/WCSasym3.net templates/predef/WCSasym3.tobs templates/predef/WCSasym4.def templates/predef/WCSasym4.net templates/predef/WCSasym4.tobs templates/predef/WCSasym5.def templates/predef/WCSasym5.net templates/predef/WCSasym5.tobs templates/predef/WCSasym6.def templates/predef/WCSasym6.net templates/predef/WCSasym6.tobs templates/predef/WCSasym8.def templates/predef/WCSasym8.net templates/predef/WCSasym8.tobs templates/predef/gen
bench/gspn-ssp/templates/WCSsym/WCSsym.def deleted 100644 → 0
View file @ 649e8e2d
|256
%
|
(C1 c 13.416667 3.266667 (@c
{@PR@}
))
(C c 13.183333 3.116667 (@c
u C1
))
(M m 13.200000 3.566667 (@m
<S C1>
))
bench/gspn-ssp/templates/WCSsym/WCSsym.net deleted 100644 → 0
View file @ 649e8e2d
|0|
|
f 0 5 0 5 0 0 0
Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C
Idle -10003 3.666667 4.083333 3.866667 4.050000 0 3.866667 4.216667 C
Wav 0 5.650000 1.916667 5.850000 1.883333 0 5.850000 2.050000 C
Att 0 7.583333 1.966667 7.783333 1.933333 0 7.783333 2.100000 C
Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C
T1 1.000000 0 0 1 0 3.650000 2.983333 3.483333 2.866667 3.816667 3.066667 0
1 2 0 0 0.000000 0.000000 <x>
1
1 1 0 0 0.000000 0.000000 <x>
0
T2 1.000000 0 0 1 1 4.683333 1.900000 4.516667 1.783333 4.850000 1.983333 0
1 1 0 0 0.000000 0.000000 <x>
1
1 3 0 0 0.000000 0.000000 <x>
2
1 4 1 0 0.000000 0.000000 <S>
5.983333 2.583333
1 5 1 0 0.000000 0.000000 <S>
5.900000 3.150000
T3 1.000000 0 0 1 1 6.583333 1.950000 6.416667 1.833333 6.750000 2.033333 0
1 3 0 0 0.000000 0.000000 <x>
1
1 4 0 0 0.000000 0.000000 <x>
0
T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0
1 4 0 0 0.000000 0.000000 <x>
1
1 5 0 0 0.000000 0.000000 <x>
2
1 5 1 0 0.000000 0.000000 <S>
10.033333 3.083333
1 3 2 0 0.000000 0.000000 <S>
10.316667 0.950000
5.650000 0.900000
T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0
1 5 0 0 0.000000 0.000000 <x>
1
1 2 0 0 0.000000 0.000000 <x>
0
bench/gspn-ssp/templates/WCSsym/WCSsym.prop deleted 100644 → 0
View file @ 649e8e2d
P1: Att >= <pr1>;
P2: Cs >= 2<pr1>;
P3: Req >= <pr1>;
P4: Idle >= 2<pr1>;
P5: Att >= 2<pr2>;
P6: #(Att) >= 2;
P7: Wav >= <pr2>;
P8: Req >= <pr2>;
bench/gspn-ssp/templates/WCSsym/gen deleted 100755 → 0
View file @ 649e8e2d
#!/bin/sh
for i in 3 4 5 6 8 ; do
sfx=$i
. templates/common
PRS=`seq 1 $i | sed 's/^/pr/;s/$/,/' | tr -d '\n' | sed 's/,$//'`
echo " sed 's/@PR@/$PRS/' '\$(srcdir)/$name/$bname.def' > '$dst/$bname$sfx.def'" >>tmp$$
echo " sed 's/:.*//' '\$(srcdir)/$name/$bname.prop' | tr '\n' ' ' > '$dst/$bname$sfx.ap'" >>tmp$$
FILES="$FILES $name/$bname.def $name/$bname.prop"
finish
done
bench/gspn-ssp/templates/bagrodia/bagrodia.def deleted 100644 → 0
View file @ 649e8e2d
|256
%
|
(x c 7.966667 1.233333 (@c
{@X@}
))
(X c 7.933333 1.033333 (@c
u x
))
(m c 8.950000 1.050000 (@c
{d,r,a}
))
(M c 8.816667 0.733333 (@c
u m
))
(Mar m 9.066667 1.450000 (@m
<S>
))
bench/gspn-ssp/templates/bagrodia/bagrodia.gd deleted 100644 → 0
View file @ 649e8e2d
r_retard[m={d} and z=MAXC(x,z)];
r_ech3[m={d} and m1={r}];
r_ech2[m={d} and m1={r} and x=MAXC(x,z)];
succ[m={d,a}];
s_retard[m={d,a} and m1={r}];
rej_retard[m={r} and m1={a}];
r_succ[m={d}];
rejet[m={r}];
dem[m={d}];
bench/gspn-ssp/templates/bagrodia/bagrodia.net deleted 100644 → 0
View file @ 649e8e2d
|0|
|
f 0 9 0 16 1 0 0
Repos -10005 2.166667 2.766667 2.366667 2.733333 0 2.366667 2.900000 X
Appel 0 4.633333 2.833333 4.833333 2.800000 0 4.833333 2.966667 X
EnCours 0 6.866667 2.783333 7.066667 2.750000 0 7.066667 2.916667 X
Pot 0 3.383333 5.016667 3.583333 4.983333 0 3.583333 5.150000 X,X
Att 0 9.550000 4.283333 9.750000 4.250000 0 9.750000 4.416667 X,X
Jeton 0 4.633333 7.416667 4.833333 7.383333 0 4.833333 7.550000 X,X
Succ 0 6.300000 9.766671 6.500000 9.733333 0 6.500000 9.900000 X,X
Retarde 0 11.850000 3.533333 12.050000 3.500000 0 12.050000 3.666667 X,X
Message 0 11.200000 7.633333 11.400000 7.600000 0 11.400000 7.766667 M,X,X
G5 0.000000 0.000000 1
r_ech1 1.000000e+00 0 0 1 0 7.783333 9.233329 7.616667 9.116667 7.950000 9.316667 0
1 9 0 0 0.000000 0.000000 <m,z,x>
1
1 9 1 0 0.000000 0.000000 <m1,x,z>
9.850000 9.300000
1
1 4 0 0 0.000000 0.000000 <x,z>
r_ech2 1.000000e+00 0 0 3 0 7.750000 8.516667 7.583333 8.400000 7.916667 8.600000 0 7.916667 8.400000 [z<>y]
1 9 0 0 0.000000 0.000000 <m,z,x>
1 4 1 0 0.000000 0.000000 <x,z>
5.933333 7.183333
1 5 1 0 0.000000 0.000000 <x,y>
9.366667 6.466667
3
1 9 1 0 0.000000 0.000000 <m1,x,z>
8.350002 8.700000
1 4 1 0 0.000000 0.000000 <x,z>
6.450000 6.883333
1 5 1 0 0.000000 0.000000 <x,y>
9.250000 6.100000
0
r_ech3 1.000000e+00 0 0 3 0 7.700000 7.150000 7.533333 7.033333 7.866667 7.233333 0 7.866667 7.033333 [z<>y]
1 8 1 0 0.000000 0.000000 <x,w>
7.850000 3.016667
1 9 0 0 0.000000 0.000000 <m,z,x>
1 5 1 0 0.000000 0.000000 <x,y>
9.100000 5.933333
3
1 9 1 0 0.000000 0.000000 <m1,x,z>
8.650000 7.816667
1 8 1 0 0.000000 0.000000 <x,w>
8.050000 3.183333
1 5 1 0 0.000000 0.000000 <x,y>
9.133333 5.400000
0
remp 1.000000e+00 0 0 1 0 4.633333 4.250000 4.466667 4.133333 4.800000 4.333333 0 4.800000 4.133333 [x <> y]
1 2 1 0 0.000000 0.000000 <x>
4.283333 3.400000
3
1 6 1 0 0.000000 0.000000 <x,y>
4.266667 6.000000
1 4 1 0 0.000000 0.000000 <x,y>
3.700000 4.316667
1 2 1 0 0.000000 0.000000 <x>
4.900000 3.500000
2
1 6 1 0 0.000000 0.000000 <x,y>
5.050000 5.916667
1 4 1 0 0.000000 0.000000 <x,y>
4.150000 4.833333
r_succ 1.000000e+00 0 0 3 1 16.266667 10.550000 16.100000 10.433333 16.433332 10.633333 0
1 9 0 0 0.000000 0.000000 <m,z,x>
1 3 1 0 0.000000 0.000000 <x>
6.866667 10.400000
1 4 1 0 0.000000 0.000000 <x,z>
3.266667 11.166667
1
1 7 1 0 0.000000 0.000000 <x,z>
11.483329 9.750000
0
rej_retard 1.000000e+00 0 0 3 1 16.200001 7.816667 16.033333 7.700000 16.366667 7.900000 0
1 8 2 0 0.000000 0.000000 <x,w>
18.083329 7.816667
18.400000 3.083333
1 9 0 0 0.000000 0.000000 <m,x,w>
1 5 0 0 0.000000 0.000000 <x,y>
2
1 9 1 0 0.000000 0.000000 <m1,x,w>
14.100000 8.350002
1 7 2 0 0.000000 0.000000 <x,w>
16.133333 9.366667
11.550000 9.516671
0
s_retard 1.000000e+00 0 0 3 1 16.033333 6.666667 15.866667 6.550000 16.200001 6.750000 0
1 8 2 0 0.000000 0.000000 <x,w>
17.366667 6.600000
17.666671 3.300000
1 9 0 0 0.000000 0.000000 <m,y,x>
1 5 0 0 0.000000 0.000000 <x,y>
2
1 9 1 0 0.000000 0.000000 <m1,x,w>
14.583333 6.550000
1 7 2 0 0.000000 0.000000 <x,y>
15.750000 9.150000
12.083333 9.566667
0
succ 1.000000e+00 0 0 2 1 15.883333 5.150000 15.716667 5.033333 16.049999 5.233333 0
1 9 0 0 0.000000 0.000000 <m,y,x>
1 5 0 0 0.000000 0.000000 <x,y>
1
1 7 2 0 0.000000 0.000000 <x,y>
15.500000 9.000000
12.316667 9.716667
1
1 8 2 0 0.000000 0.000000 <x,S>
16.750000 4.983333
16.799999 3.533333
vide_J 1.000000e+00 0 0 2 0 5.066667 9.366667 4.900000 9.250000 5.233333 9.450000 0
1 7 1 0 0.000000 0.000000 <x,y>
6.033333 9.383333
1 6 1 0 0.000000 0.000000 <x,z>
5.016667 7.966667
1
1 7 1 0 0.000000 0.000000 <x,y>
5.533333 9.566667
0
fin 1.000000e+00 0 0 1 1 2.716667 9.816667 2.550000 9.700000 2.883333 9.900000 0
1 7 0 0 0.000000 0.000000 <x,y>
1
1 1 1 0 0.000000 0.000000 <x>
2.233333 9.833333
2
1 4 1 0 0.000000 0.000000 <x,S>
2.416667 9.583333
1 6 1 0 0.000000 0.000000 <x,S>
3.866667 9.683333
vide_p 1.000000e+00 0 0 2 0 3.633333 8.650000 3.466667 8.533333 3.800000 8.733333 0
1 7 1 0 0.000000 0.000000 <x,z>