diff --git a/ChangeLog b/ChangeLog index 55fda08ff..01b91064c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2008-08-07 Alexandre Duret-Lutz + + * bench/gspn-ssp/Makefile.am, bench/gspn-ssp/trans2prop.pl: New files. + * bench/gspn-ssp/config: Rename as bench/gspn-ssp/defs.in. + * bench/Makefile.am (SUBDIRS): Add gspn-ssp. + * configure.ac: Output bench/gspn-ssp/Makefile and bench/gspn-ssp/defs. + * bench/gspn-ssp/bench: Include defs. + +2008-08-07 Alexandre Duret-Lutz + + * bench/gspn-ssp/: New directory. Contains some of the benches + used in baarir.06.tr03, baarir.07.acsd, and baarir.07.msr. + 2008-08-07 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc: New option: -e54. diff --git a/bench/Makefile.am b/bench/Makefile.am index ae7fe900f..939b98804 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -19,4 +19,4 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -SUBDIRS = emptchk ltl2tgba +SUBDIRS = emptchk gspn-ssp ltl2tgba diff --git a/bench/gspn-ssp/Makefile.am b/bench/gspn-ssp/Makefile.am new file mode 100644 index 000000000..0a933e050 --- /dev/null +++ b/bench/gspn-ssp/Makefile.am @@ -0,0 +1,64 @@ +## Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## 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. + +EXTRA_DIST = \ + bench \ + benchaux \ + gen \ + sum \ + sumall \ + templates/bagrodia/bagrodia.con \ + templates/bagrodia/bagrodia.def \ + templates/bagrodia/bagrodia.gd \ + templates/bagrodia/bagrodia.net \ + templates/bagrodia/bagrodia.prop \ + templates/bagrodia/gen \ + templates/common \ + templates/gen \ + templates/predef/gen \ + templates/predef/WCSasym10.def \ + templates/predef/WCSasym10.net \ + templates/predef/WCSasym10.tobs \ + templates/predef/WCSasym2.def \ + templates/predef/WCSasym2.net \ + templates/predef/WCSasym2.tobs \ + 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/WCSsym/gen \ + templates/WCSsym/WCSsym.con \ + templates/WCSsym/WCSsym.def \ + templates/WCSsym/WCSsym.gd \ + templates/WCSsym/WCSsym.net \ + templates/WCSsym/WCSsym.prop \ + trans2prop.pl diff --git a/bench/gspn-ssp/bench b/bench/gspn-ssp/bench new file mode 100755 index 000000000..a72fcf33f --- /dev/null +++ b/bench/gspn-ssp/bench @@ -0,0 +1,23 @@ +#!/bin/sh +. ./defs +H=`pwd` +test -d results || mkdir results +cd models +[ $# -eq 0 ] && set -- * +for i; do + cd $i + for ltl2tgba in -f; do + case $i in + *.rg) checks=e2;; + *) checks='e4 e6 e5 e5L e5n e2 e45 e45n';; + esac + for check in $checks; do + res=$H/results/$i.RES-$check$ltl2tgba + test -f $res && continue + export res check i ltl2tgba + rm -f $res + $TIME "$H/benchaux" 2>$res-TOTAL + done + done + cd .. +done diff --git a/bench/gspn-ssp/benchaux b/bench/gspn-ssp/benchaux new file mode 100755 index 000000000..bc0d42bfe --- /dev/null +++ b/bench/gspn-ssp/benchaux @@ -0,0 +1,40 @@ +#!/bin/sh -x +case $check in + *L) check="${check%L} -L";; + *n) check="${check%n} -n";; +esac +set -x +$RANDLTL -F 50 -u -s 0 -f 10 -r 7 `cat $i.ap` | +while read f; do + echo "Running with $f on $i with -$check $ltl2tgba" + (case $i in + *.rg) + if [ ! -f $i.snow ]; then + $TIME $LTLGSPNSRG -$check $ltl2tgba $i "$f" `cat $i.ap` 2>&1 + else + PROPS=`echo $f | sed 's/P[0-9]/&,\n/g' | sed 's/.*P/P/' | + grep P | sort -u | tr -d '\n' | sed 's/,$//'` + $SNOW -m $i.cami -p $i.snow -f "$PROPS" + $TRANS2PL model + mv model.nettmp model.net + $TIME $LTLGSPNSRG -$check $ltl2tgba model "$f" \ + `echo $PROPS | tr ',' ' '` 2>&1 + fi;; + *) + $TIME $LTLGSPNSSP -$check $ltl2tgba $i "$f" "$i.con" `cat $i.ap` 2>&1 ;; + esac + test -f *.mark || touch "x.mark" + test -f *.event || touch "x.event" + du -b *.mark *.event | cut -f 1 + ) | + tee tmp + sed -n '/^$/n; + /^Command exited with non-zero status/n; + 2,$s/[^0-9.]//g; + s/^[.]//; + 1x; + 2,$H; + $x; + $s/\n/,/g; + $p' < tmp >> $res +done diff --git a/bench/gspn-ssp/defs.in b/bench/gspn-ssp/defs.in new file mode 100644 index 000000000..441ff26ea --- /dev/null +++ b/bench/gspn-ssp/defs.in @@ -0,0 +1,43 @@ +# -*- shell-script -*- +# Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# 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='@top_builddir@/src/ltltest/randltl' +LTLGSPNSSP='@top_builddir@/iface/gspn/ltlgspn-ssp' +LTLGSPNSRG='@top_builddir@/iface/gspn/ltlgspn-srg' +SNOW=/home/adl/projs/src/gspn/snow +TRANS2PL='@srcdir@/trans2prop.pl' +TIME='/usr/bin/time -p' +export RANDLTL LTLGSPNSSP LTLGSPNSRG TIME SNOW TRANS2PL diff --git a/bench/gspn-ssp/gen b/bench/gspn-ssp/gen new file mode 100755 index 000000000..17f8de75c --- /dev/null +++ b/bench/gspn-ssp/gen @@ -0,0 +1,2 @@ +#!/bin/sh +cd templates && ./gen diff --git a/bench/gspn-ssp/sum b/bench/gspn-ssp/sum new file mode 100755 index 000000000..d0ce530dd --- /dev/null +++ b/bench/gspn-ssp/sum @@ -0,0 +1,232 @@ +#!/usr/bin/env perl + +use warnings; +use strict; + +my %C = ( + e2 => [ + "formulae", + "unique states visited", + "SCC in search stack", + "max. depth", + "removed components", + "states", + "transitions", + "vmsize", + "real", + "user", + "sys", + ".mark size", + ".event size", + "mem total", + ], + e4 => [ + "formulae", + "unique states visited", + "SCC in search stack", + "contained map size", + "find_state count", + "max. depth", + "removed components", + "states", + "transitions", + "vmsize", + "real", + "user", + "sys", + ".mark size", + ".event size", + "mem total", + ], + e45 => [ + "formulae", + "unique states visited", + "SCC in search stack", + "contained map size", + "inclusion count heap", + "inclusion count stack", + "max. depth", + "removed components", + "states", + "transitions", + "vmsize", + "real", + "user", + "sys", + ".mark size", + ".event size", + "mem total", + ], + e5 => [ + "formulae", + "unique states visited", + "SCC in search stack", + "contained map size", + "inclusion count heap", + "inclusion count stack", + "max. depth", + "removed components", + "states", + "transitions", + "vmsize", + "real", + "user", + "sys", + ".mark size", + ".event size", + "mem total", + ], + e6 => [ + "formulae", + "unique states visited", + "SCC in search stack", + "contained map size", + "inclusion count heap", + "inclusion count stack", + "max. depth", + "removed components", + "states", + "transitions", + "vmsize", + "real", + "user", + "sys", + ".mark size", + ".event size", + "mem total", + ], + ); + +my %filter = (states => 1, transitions => 1, user => 1); +my %order = (e2 => 2, e6 => 3, e5 => 4, e4 => 5); + + +my %H; +my %S; +my %P; + +while (<>) +{ + my @l = split (/,/); + + push @l, ($l[-1] + $l[-2] + $l[-6] * 4096)/1024; + + my $e = shift @l; + $e =~ s/non empty/non e./; + + $ARGV =~ /([\w.]+).RES-(\w+)/; + my $name = $1; + my $meth = $2; + $meth =~ s/[nL]$//; + + $P{$name}{$e}{$meth} = 1; + + if (!exists $H{$meth}{$ARGV}{$e}) + { + $H{$meth}{$ARGV}{$e} = [1, @l]; + $S{$meth} = 1 + @l; + } + else + { + $H{$meth}{$ARGV}{$e}->[0]++; + for (my $i = 0; $i < @l; ++$i) + { + $H{$meth}{$ARGV}{$e}->[$i + 1] += $l[$i]; + } + } +} + +sub model_sort ($$) +{ + my ($a, $b) = @_; + $a =~ s/\.rg//; + $a =~ s/.*(\d)$/$1$&/; + $b =~ s/\.rg//; + $b =~ s/.*(\d)$/$1$&/; + return $a cmp $b; +}; + +if (exists $ENV{FORTETABLE}) +{ + foreach my $e ("non e.", "empty") + { + foreach my $model (sort model_sort keys %P) + { + if (exists $P{$model}{$e}) + { + foreach my $meth (sort { $order{$a} <=> $order{$b} } + keys %{$P{$model}{$e}}) + { + my $n = "results/$model.RES-$meth-f"; + next unless exists $H{$meth}{$n}{$e}; + my @l = @{$H{$meth}{$n}{$e}}; + print " "x17 . "% $model $meth $e\n"; + my $st = $l[-5]/$l[0]; + my $tr = $l[-4]/$l[0]; + my $T = $l[-2]/$l[0]; + my $res = $T >= 10 ? 1 : 2; + $res = 0 if $T >= 100; + printf "%17s& %.0f & %.0f & %.${res}f\n", "", $st, $tr, $T; + } + } + } + } + + + + #if not exists $filter{$C{$meth}->[$i]}; + + exit 0; +} + + + +foreach my $meth (sort keys %H) +{ + printf "%21s", ""; + foreach my $n (sort keys %{$H{$meth}}) + { + $n =~ s,.*/,,; + $n =~ s,\.RES,,; + $n =~ s,-f,,; + printf "%18s", $n; + } + print "\n"; + + printf "%21s", ""; + foreach my $n (sort keys %{$H{$meth}}) + { + my $x = 2; + foreach my $k (keys %{$H{$meth}{$n}}) + { + printf "%9s", $k; + $x--; + } + print " " x (9*$x); + } + print "\n"; + + for (my $i = 0; $i < $S{$meth}; ++$i) + { + printf "%-22s", $C{$meth}->[$i]; + foreach my $n (sort keys %{$H{$meth}}) + { + my $x = 2; + foreach my $k (keys %{$H{$meth}{$n}}) + { + my @l = @{$H{$meth}{$n}{$k}}; + if ($i) + { + printf "%8.2f ", $l[$i]/$l[0]; + } + else + { + printf "%5dx ", $l[$i]; + } + $x-- + } + print " " x (9*$x); + } + print "\n"; + } +} diff --git a/bench/gspn-ssp/sumall b/bench/gspn-ssp/sumall new file mode 100755 index 000000000..823c38ea8 --- /dev/null +++ b/bench/gspn-ssp/sumall @@ -0,0 +1,13 @@ +#!/bin/sh + +[ $# -eq 0 ] && set results/*.RES-* + +for i; do + case $i in + *-TOTAL);; + *) + x="$x $i"; + ;; + esac +done +./sum $x diff --git a/bench/gspn-ssp/templates/WCSsym/WCSsym.con b/bench/gspn-ssp/templates/WCSsym/WCSsym.con new file mode 100644 index 000000000..8ef29b59c --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/WCSsym.con @@ -0,0 +1 @@ +"1","1","1",; diff --git a/bench/gspn-ssp/templates/WCSsym/WCSsym.def b/bench/gspn-ssp/templates/WCSsym/WCSsym.def new file mode 100644 index 000000000..6a647ca46 --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/WCSsym.def @@ -0,0 +1,12 @@ +|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 + +)) diff --git a/bench/gspn-ssp/templates/WCSsym/WCSsym.gd b/bench/gspn-ssp/templates/WCSsym/WCSsym.gd new file mode 100644 index 000000000..a5fa92f9e --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/WCSsym.gd @@ -0,0 +1 @@ +T6[MAXIMUM(x)]; diff --git a/bench/gspn-ssp/templates/WCSsym/WCSsym.net b/bench/gspn-ssp/templates/WCSsym/WCSsym.net new file mode 100644 index 000000000..c2777b6ed --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/WCSsym.net @@ -0,0 +1,48 @@ +|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 + 1 + 1 1 0 0 0.000000 0.000000 + 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 + 1 + 1 3 0 0 0.000000 0.000000 + 2 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 + 1 5 1 0 0.000000 0.000000 +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 + 1 + 1 4 0 0 0.000000 0.000000 + 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 + 1 + 1 5 0 0 0.000000 0.000000 + 2 + 1 5 1 0 0.000000 0.000000 +10.033333 3.083333 + 1 3 2 0 0.000000 0.000000 +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 + 1 + 1 2 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/WCSsym/WCSsym.prop b/bench/gspn-ssp/templates/WCSsym/WCSsym.prop new file mode 100644 index 000000000..045b962b6 --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/WCSsym.prop @@ -0,0 +1,8 @@ +P1: Att >= ; +P2: Cs >= 2; +P3: Req >= ; +P4: Idle >= 2; +P5: Att >= 2; +P6: #(Att) >= 2; +P7: Wav >= ; +P8: Req >= ; diff --git a/bench/gspn-ssp/templates/WCSsym/gen b/bench/gspn-ssp/templates/WCSsym/gen new file mode 100755 index 000000000..febd7319e --- /dev/null +++ b/bench/gspn-ssp/templates/WCSsym/gen @@ -0,0 +1,8 @@ +#!/bin/sh +for i in 3 4 5 6 8 ; do + sfx=$i + . ../common + PRS=`seq 1 $i | sed 's/^/pr/;s/$/,/' | tr -d '\n' | sed 's/,$//'` + sed "s/@PR@/$PRS/" "$name.def" > "$dst/$name$sfx.def" + sed "s/:.*//" < "$name.prop" | tr '\n' ' ' > "$dst/$name$sfx.ap" +done diff --git a/bench/gspn-ssp/templates/bagrodia/bagrodia.con b/bench/gspn-ssp/templates/bagrodia/bagrodia.con new file mode 100644 index 000000000..8ef29b59c --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/bagrodia.con @@ -0,0 +1 @@ +"1","1","1",; diff --git a/bench/gspn-ssp/templates/bagrodia/bagrodia.def b/bench/gspn-ssp/templates/bagrodia/bagrodia.def new file mode 100644 index 000000000..9ddce71c3 --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/bagrodia.def @@ -0,0 +1,18 @@ +|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 + +)) diff --git a/bench/gspn-ssp/templates/bagrodia/bagrodia.gd b/bench/gspn-ssp/templates/bagrodia/bagrodia.gd new file mode 100644 index 000000000..232a1b9fe --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/bagrodia.gd @@ -0,0 +1,9 @@ +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}]; diff --git a/bench/gspn-ssp/templates/bagrodia/bagrodia.net b/bench/gspn-ssp/templates/bagrodia/bagrodia.net new file mode 100644 index 000000000..f8b76f66c --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/bagrodia.net @@ -0,0 +1,193 @@ +|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 + 1 + 1 9 1 0 0.000000 0.000000 +9.850000 9.300000 + 1 + 1 4 0 0 0.000000 0.000000 +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 + 1 4 1 0 0.000000 0.000000 +5.933333 7.183333 + 1 5 1 0 0.000000 0.000000 +9.366667 6.466667 + 3 + 1 9 1 0 0.000000 0.000000 +8.350002 8.700000 + 1 4 1 0 0.000000 0.000000 +6.450000 6.883333 + 1 5 1 0 0.000000 0.000000 +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 +7.850000 3.016667 + 1 9 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.100000 5.933333 + 3 + 1 9 1 0 0.000000 0.000000 +8.650000 7.816667 + 1 8 1 0 0.000000 0.000000 +8.050000 3.183333 + 1 5 1 0 0.000000 0.000000 +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 +4.283333 3.400000 + 3 + 1 6 1 0 0.000000 0.000000 +4.266667 6.000000 + 1 4 1 0 0.000000 0.000000 +3.700000 4.316667 + 1 2 1 0 0.000000 0.000000 +4.900000 3.500000 + 2 + 1 6 1 0 0.000000 0.000000 +5.050000 5.916667 + 1 4 1 0 0.000000 0.000000 +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 + 1 3 1 0 0.000000 0.000000 +6.866667 10.400000 + 1 4 1 0 0.000000 0.000000 +3.266667 11.166667 + 1 + 1 7 1 0 0.000000 0.000000 +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 +18.083329 7.816667 +18.400000 3.083333 + 1 9 0 0 0.000000 0.000000 + 1 5 0 0 0.000000 0.000000 + 2 + 1 9 1 0 0.000000 0.000000 +14.100000 8.350002 + 1 7 2 0 0.000000 0.000000 +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 +17.366667 6.600000 +17.666671 3.300000 + 1 9 0 0 0.000000 0.000000 + 1 5 0 0 0.000000 0.000000 + 2 + 1 9 1 0 0.000000 0.000000 +14.583333 6.550000 + 1 7 2 0 0.000000 0.000000 +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 + 1 5 0 0 0.000000 0.000000 + 1 + 1 7 2 0 0.000000 0.000000 +15.500000 9.000000 +12.316667 9.716667 + 1 + 1 8 2 0 0.000000 0.000000 +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 +6.033333 9.383333 + 1 6 1 0 0.000000 0.000000 +5.016667 7.966667 + 1 + 1 7 1 0 0.000000 0.000000 +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 + 1 + 1 1 1 0 0.000000 0.000000 +2.233333 9.833333 + 2 + 1 4 1 0 0.000000 0.000000 +2.416667 9.583333 + 1 6 1 0 0.000000 0.000000 +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 +6.283333 8.533333 + 1 4 1 0 0.000000 0.000000 +3.650000 5.766667 + 1 + 1 7 1 0 0.000000 0.000000 +6.033333 8.900000 + 0 +dem 1.000000e+00 0 0 3 1 7.650000 4.283333 7.483333 4.166667 7.816667 4.366667 0 + 1 4 1 0 0.000000 0.000000 +5.833333 4.066667 + 1 6 0 0 0.000000 0.000000 + 1 3 0 0 0.000000 0.000000 + 3 + 1 9 1 0 0.000000 0.000000 +10.783333 5.833333 + 1 5 0 0 0.000000 0.000000 + 1 4 1 0 0.000000 0.000000 +6.150000 4.650000 + 0 +rejet 1.000000e+00 0 0 2 1 8.650000 2.633333 8.483333 2.516667 8.816667 2.716667 0 + 1 9 1 0 0.000000 0.000000 +11.150000 2.450000 + 1 5 1 0 0.000000 0.000000 +9.466667 2.666667 + 1 + 1 3 0 0 0.000000 0.000000 + 1 + 1 8 0 0 0.000000 0.000000 +pret 1.000000e+00 0 0 1 1 5.950000 2.833333 5.783333 2.716667 6.116667 2.916667 0 + 1 2 0 0 0.000000 0.000000 + 1 + 1 3 0 0 0.000000 0.000000 + 0 +Session 1.000000e+00 0 0 1 1 3.466667 2.783333 3.300000 2.666667 3.633333 2.866667 0 + 1 1 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +r_retard 1.000000e+00 1 1 3 0 7.683333 5.933333 7.516667 5.816667 7.850000 6.016667 0 7.850000 5.816667 [z <> y] + 1 9 0 0 0.000000 0.000000 + 1 4 1 0 0.000000 0.000000 +6.216667 5.033333 + 1 5 1 0 0.000000 0.000000 +9.016671 5.316667 + 3 + 1 8 1 0 0.000000 0.000000 +8.500000 3.400000 + 1 4 1 0 0.000000 0.000000 +6.000000 5.650000 + 1 5 0 0 0.000000 0.000000 + 1 + 1 8 1 0 0.000000 0.000000 +8.700000 3.866667 diff --git a/bench/gspn-ssp/templates/bagrodia/bagrodia.prop b/bench/gspn-ssp/templates/bagrodia/bagrodia.prop new file mode 100644 index 000000000..872913d97 --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/bagrodia.prop @@ -0,0 +1,8 @@ +P1: Repos >= + ; +P2: Pot >= ; +P3: Att >= ; +P4: Appel >= 2; +P5: EnCours >= 2; +P6: EnCours >= ; +P7: #(Jeton) >= 2; +P8: [-,*,-](Message) >= ; diff --git a/bench/gspn-ssp/templates/bagrodia/gen b/bench/gspn-ssp/templates/bagrodia/gen new file mode 100755 index 000000000..33965e1b8 --- /dev/null +++ b/bench/gspn-ssp/templates/bagrodia/gen @@ -0,0 +1,8 @@ +#!/bin/sh +for i in 2; do + sfx=$i + . ../common + X=`seq 1 $i | sed 's/^/x/;s/$/,/' | tr -d '\n' | sed 's/,$//'` + sed "s/@X@/$X/" "$name.def" > "$dst/$name$sfx.def" + sed "s/:.*//" < "$name.prop" | tr '\n' ' ' > "$dst/$name$sfx.ap" +done diff --git a/bench/gspn-ssp/templates/common b/bench/gspn-ssp/templates/common new file mode 100644 index 000000000..e56c5ec80 --- /dev/null +++ b/bench/gspn-ssp/templates/common @@ -0,0 +1,7 @@ +name=$(basename $(pwd)) +dst=../../models/$name$sfx +mkdir "$dst" +for ext in con net prop; do + cp "$name".$ext "$dst/$name$sfx.$ext" +done +test -f "$name".gd && cp "$name".gd "$dst/$name$sfx.gd" diff --git a/bench/gspn-ssp/templates/gen b/bench/gspn-ssp/templates/gen new file mode 100755 index 000000000..2927c4f4b --- /dev/null +++ b/bench/gspn-ssp/templates/gen @@ -0,0 +1,6 @@ +#!/bin/sh +rm -Rf ../models +mkdir ../models +for dir in predef WCSsym bagrodia s2j2t2 s2j3t2 s3j2t2; do + (cd $dir && ./gen) +done diff --git a/bench/gspn-ssp/templates/predef/WCSasym10.def b/bench/gspn-ssp/templates/predef/WCSasym10.def new file mode 100644 index 000000000..088254274 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym10.def @@ -0,0 +1,39 @@ +|256 +% +| +(C1 c 22.808333 5.553334 (@c +{pr1} +)) +(C2 c 22.808333 5.808333 (@c +{pr2} +)) +(C c 22.411666 5.298333 (@c +u C1,C2,C3,C4,C5,C6,C7,C8,C9,C10 +)) +(C3 c 22.808333 6.120000 (@c +{pr3} +)) +(M m 22.496667 8.103334 (@m ++++++++++ +)) +(C4 c 22.808333 6.375000 (@c +{pr4} +)) +(C5 c 22.808333 6.630000 (@c +{pr5} +)) +(C6 c 22.808333 6.885000 (@c +{pr6} +)) +(C7 c 22.808333 7.140000 (@c +{pr7} +)) +(C8 c 22.808333 7.395000 (@c +{pr8} +)) +(C9 c 22.800000 7.566667 (@c +{pr9} +)) +(C10 c 22.800000 7.766667 (@c +{pr10} +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym10.net b/bench/gspn-ssp/templates/predef/WCSasym10.net new file mode 100644 index 000000000..511d94e35 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym10.net @@ -0,0 +1,64 @@ +|0| + + +| +f 0 6 0 7 1 0 0 +Req 0 6.290000 3.230000 6.630000 3.173334 0 6.630000 3.456666 C +Idle -10005 6.233334 6.941666 6.573334 6.885000 0 6.573334 7.168334 C +Wav 0 9.605000 3.258334 9.945000 3.201666 0 9.945000 3.485000 C +Att 0 12.891666 3.343334 13.231666 3.286666 0 13.231666 3.570000 C +Sel 0 15.696663 3.286666 16.036667 3.230000 0 16.036667 3.513334 C +Cs 0 17.765000 7.083334 18.105000 7.026667 0 18.105000 7.310000 C +G11 0.000000 0.000000 1 +T1 1.000000 0 0 1 0 6.205000 5.071666 5.921666 4.873334 6.488334 5.213334 0 + 1 2 0 0 0.000000 0.000000 + 1 + 1 1 0 0 0.000000 0.000000 + 0 +T2 1.000000 0 0 1 1 7.961666 3.230000 7.678334 3.031666 8.245000 3.371666 0 + 1 1 0 0 0.000000 0.000000 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +10.171666 4.391666 + 1 6 1 0 0.000000 0.000000 +10.030000 5.355000 + 1 5 2 0 0.000000 0.000000 +10.001666 4.930000 +15.555000 5.666666 +T3 1.000000 0 0 1 1 11.191666 3.315000 10.908334 3.116666 11.475000 3.456666 0 + 1 3 0 0 0.000000 0.000000 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 14.308334 3.343334 14.025000 3.145000 14.591666 3.485000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +14.903334 2.635000 +T6 1.000000 0 0 1 1 17.680001 3.286666 17.396666 3.088334 17.963334 3.428334 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +14.223334 1.983334 + 1 6 1 0 0.000000 0.000000 +17.056667 5.241666 +T7 1.000000 0 0 1 1 12.126666 6.941666 11.843334 6.743334 12.410000 7.083334 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 14.336667 4.136666 13.855000 3.626666 14.620001 4.278334 0 14.620001 3.938334 [d(x)=C10 or (d(x)=C9 and (d(y)=8 or d(y)=C7 or d(y)=C6 or d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C8 and (d(y)=C7 or d(y)=C6 or d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C7 and (d(y)=C6 or d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or(d(x)=C6 and (d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1))or(d(x)=C5 and (d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1))or(d(x)=C4 and (d(y)=C3 or d(y)=C2 or d(y)=C1))or(d(x)=C3 and (d(y)=C2 or d(y)=C1)) or(d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +15.498334 4.646666 + 2 + 1 4 1 0 0.000000 0.000000 +13.061666 4.561666 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym10.tobs b/bench/gspn-ssp/templates/predef/WCSasym10.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym10.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym2.def b/bench/gspn-ssp/templates/predef/WCSasym2.def new file mode 100644 index 000000000..e0fd14218 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym2.def @@ -0,0 +1,15 @@ +|256 +% +| +(C1 c 12.350000 1.666667 (@c +{pr1} +)) +(C2 c 12.350000 1.833333 (@c +{pr2} +)) +(C c 12.150000 1.483333 (@c +u C1,C2 +)) +(M m 12.250000 2.383333 (@m ++ +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym2.net b/bench/gspn-ssp/templates/predef/WCSasym2.net new file mode 100644 index 000000000..fe37cd0a5 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym2.net @@ -0,0 +1,63 @@ +|0| + +| +f 0 6 0 7 1 0 0 +Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C +Idle -10004 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 +Sel 0 9.233332 1.933333 9.433333 1.900000 0 9.433333 2.066667 C +Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C +G2 0.000000 0.000000 1 +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 + 1 + 1 1 0 0 0.000000 0.000000 + 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 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 5 2 0 0.000000 0.000000 +5.883333 2.900000 +9.150000 3.333333 + 1 6 1 0 0.000000 0.000000 +5.900000 3.150000 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 +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 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 8.416667 1.966667 8.250000 1.850000 8.583333 2.050000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +8.800000 1.566667 +T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 6 1 0 0.000000 0.000000 +10.033333 3.083333 + 1 3 1 0 0.000000 0.000000 +8.366667 1.166667 +T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 8.400000 2.616667 8.116666 2.316667 8.566667 2.700001 0 8.566667 2.500001 [d(x)=C2 and d(y)=C1] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.116667 2.733333 + 2 + 1 4 1 0 0.000000 0.000000 +7.683333 2.683333 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym2.tobs b/bench/gspn-ssp/templates/predef/WCSasym2.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym2.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym3.def b/bench/gspn-ssp/templates/predef/WCSasym3.def new file mode 100644 index 000000000..5d0fa14ee --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym3.def @@ -0,0 +1,18 @@ +|256 +% +| +(C1 c 12.350000 1.666667 (@c +{pr1} +)) +(C2 c 12.350000 1.833333 (@c +{pr2} +)) +(C c 12.150000 1.483333 (@c +u C1,C2,C3 +)) +(C3 c 12.350000 1.983333 (@c +{pr3} +)) +(M m 12.250000 2.383333 (@m +++ +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym3.net b/bench/gspn-ssp/templates/predef/WCSasym3.net new file mode 100644 index 000000000..2237000ba --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym3.net @@ -0,0 +1,64 @@ +|0| + + +| +f 0 6 0 7 1 0 0 +Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C +Idle -10005 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 +Sel 0 9.233331 1.933333 9.433333 1.900000 0 9.433333 2.066667 C +Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C +G2 0.000000 0.000000 1 +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 + 1 + 1 1 0 0 0.000000 0.000000 + 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 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 + 1 6 1 0 0.000000 0.000000 +5.900000 3.150000 + 1 5 2 0 0.000000 0.000000 +5.883333 2.900000 +9.150000 3.333333 +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 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 8.416667 1.966667 8.250000 1.850000 8.583333 2.050000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +8.766667 1.550000 +T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +8.366667 1.166667 + 1 6 1 0 0.000000 0.000000 +10.033333 3.083333 +T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 8.433333 2.433333 8.150000 2.133333 8.600000 2.516667 0 8.600000 2.316667 [d(x)=C3 or (d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.116667 2.733333 + 2 + 1 4 1 0 0.000000 0.000000 +7.683333 2.683333 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym3.tobs b/bench/gspn-ssp/templates/predef/WCSasym3.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym3.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym4.def b/bench/gspn-ssp/templates/predef/WCSasym4.def new file mode 100644 index 000000000..1d2c47627 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym4.def @@ -0,0 +1,21 @@ +|256 +% +| +(C1 c 12.350000 1.666667 (@c +{pr1} +)) +(C2 c 12.350000 1.833333 (@c +{pr2} +)) +(C c 12.150000 1.483333 (@c +u C1,C2,C3,C4 +)) +(C3 c 12.350000 1.983333 (@c +{pr3} +)) +(C4 c 12.350000 1.983333 (@c +{pr4} +)) +(M m 12.250000 2.383333 (@m ++++ +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym4.net b/bench/gspn-ssp/templates/predef/WCSasym4.net new file mode 100644 index 000000000..ae2309d19 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym4.net @@ -0,0 +1,66 @@ +|0| + + + + +| +f 0 6 0 7 1 0 0 +Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C +Idle -10006 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 +Sel 0 9.233329 1.933333 9.433333 1.900000 0 9.433333 2.066667 C +Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C +G3 0.000000 0.000000 1 +T1 1.000000e+00 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 + 1 + 1 1 0 0 0.000000 0.000000 + 0 +T2 1.000000e+00 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 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 + 1 6 1 0 0.000000 0.000000 +5.900000 3.150000 + 1 5 2 0 0.000000 0.000000 +5.883333 2.900000 +9.150000 3.333333 +T3 1.000000e+00 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 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000e+00 0 0 1 1 8.416667 1.966667 8.250000 1.850000 8.583333 2.050000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +8.766669 1.550000 +T6 1.000000e+00 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +8.366667 1.166667 + 1 6 1 0 0.000000 0.000000 +10.033333 3.083333 +T7 1.000000e+00 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000e+00 1 1 2 1 8.433333 2.433333 8.150000 2.133333 8.600000 2.516667 0 8.600000 2.316667 [d(x)=C4 or (d(x)=C3 and ( d(y)=C2 or d(y)=C1)) or (d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.116667 2.733333 + 2 + 1 4 1 0 0.000000 0.000000 +7.683333 2.683333 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym4.tobs b/bench/gspn-ssp/templates/predef/WCSasym4.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym4.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym5.def b/bench/gspn-ssp/templates/predef/WCSasym5.def new file mode 100644 index 000000000..107579f68 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym5.def @@ -0,0 +1,24 @@ +|256 +% +| +(C1 c 13.416667 3.266667 (@c +{pr1} +)) +(C2 c 13.416667 3.416667 (@c +{pr2} +)) +(C c 13.183333 3.116667 (@c +u C1,C2,C3,C4,C5 +)) +(C3 c 13.416667 3.600000 (@c +{pr3} +)) +(M m 13.233333 4.766667 (@m +++++ +)) +(C4 c 13.416667 3.750000 (@c +{pr4} +)) +(C5 c 13.416667 3.900000 (@c +{pr5} +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym5.net b/bench/gspn-ssp/templates/predef/WCSasym5.net new file mode 100644 index 000000000..42e471181 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym5.net @@ -0,0 +1,64 @@ +|0| + + +| +f 0 6 0 7 1 0 0 +Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C +Idle -10005 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 +Sel 0 9.233331 1.933333 9.433333 1.900000 0 9.433333 2.066667 C +Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C +G6 0.000000 0.000000 1 +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 + 1 + 1 1 0 0 0.000000 0.000000 + 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 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 + 1 6 1 0 0.000000 0.000000 +5.900000 3.150000 + 1 5 2 0 0.000000 0.000000 +5.883333 2.900000 +9.150000 3.333333 +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 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 8.416667 1.966667 8.250000 1.850000 8.583333 2.050000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +8.766667 1.550000 +T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +8.366667 1.166667 + 1 6 1 0 0.000000 0.000000 +10.033333 3.083333 +T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 8.433333 2.433333 8.150000 2.133333 8.600000 2.516667 0 8.600000 2.316667 [d(x)=C5 or (d(x)=C4 and (d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C3 and (d(y)=C2 or d(y)=C1)) or (d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.116667 2.733333 + 2 + 1 4 1 0 0.000000 0.000000 +7.683333 2.683333 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym5.tobs b/bench/gspn-ssp/templates/predef/WCSasym5.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym5.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym6.def b/bench/gspn-ssp/templates/predef/WCSasym6.def new file mode 100644 index 000000000..1c0453405 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym6.def @@ -0,0 +1,27 @@ +|256 +% +| +(C1 c 13.416667 3.266667 (@c +{pr1} +)) +(C2 c 13.416667 3.416667 (@c +{pr2} +)) +(C c 13.183333 3.116667 (@c +u C1,C2,C3,C4,C5,C6 +)) +(C3 c 13.416667 3.600000 (@c +{pr3} +)) +(M m 13.233333 4.766667 (@m ++++++ +)) +(C4 c 13.416667 3.750000 (@c +{pr4} +)) +(C5 c 13.416667 3.900000 (@c +{pr5} +)) +(C6 c 13.416667 4.050000 (@c +{pr6} +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym6.net b/bench/gspn-ssp/templates/predef/WCSasym6.net new file mode 100644 index 000000000..2c957e735 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym6.net @@ -0,0 +1,64 @@ +|0| + + +| +f 0 6 0 7 1 0 0 +Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C +Idle -10005 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 +Sel 0 9.233331 1.933333 9.433333 1.900000 0 9.433333 2.066667 C +Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C +G7 0.000000 0.000000 1 +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 + 1 + 1 1 0 0 0.000000 0.000000 + 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 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +5.983333 2.583333 + 1 6 1 0 0.000000 0.000000 +5.900000 3.150000 + 1 5 2 0 0.000000 0.000000 +5.883333 2.900000 +9.150000 3.333333 +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 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 8.416667 1.966667 8.250000 1.850000 8.583333 2.050000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +8.766667 1.550000 +T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +8.366667 1.166667 + 1 6 1 0 0.000000 0.000000 +10.033333 3.083333 +T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 8.433333 2.433333 8.150000 2.133333 8.600000 2.516667 0 8.600000 2.316667 [d(x)=C6 or (d(x)=C5 and (d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C4 and (d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C3 and (d(y)=C2 or d(y)=C1)) or(d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +9.116667 2.733333 + 2 + 1 4 1 0 0.000000 0.000000 +7.683333 2.683333 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym6.tobs b/bench/gspn-ssp/templates/predef/WCSasym6.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym6.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym8.def b/bench/gspn-ssp/templates/predef/WCSasym8.def new file mode 100644 index 000000000..a210bcf16 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym8.def @@ -0,0 +1,33 @@ +|256 +% +| +(C1 c 22.808333 5.553334 (@c +{pr1} +)) +(C2 c 22.808333 5.808333 (@c +{pr2} +)) +(C c 22.411666 5.298333 (@c +u C1,C2,C3,C4,C5,C6,C7,C8 +)) +(C3 c 22.808333 6.120000 (@c +{pr3} +)) +(M m 22.496667 8.103334 (@m ++++++++ +)) +(C4 c 22.808333 6.375000 (@c +{pr4} +)) +(C5 c 22.808333 6.630000 (@c +{pr5} +)) +(C6 c 22.808333 6.885000 (@c +{pr6} +)) +(C7 c 22.808333 7.140000 (@c +{pr7} +)) +(C8 c 22.808333 7.395000 (@c +{pr8} +)) diff --git a/bench/gspn-ssp/templates/predef/WCSasym8.net b/bench/gspn-ssp/templates/predef/WCSasym8.net new file mode 100644 index 000000000..efd54786d --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym8.net @@ -0,0 +1,64 @@ +|0| + + +| +f 0 6 0 7 1 0 0 +Req 0 6.290000 3.230000 6.630000 3.173334 0 6.630000 3.456666 C +Idle -10005 6.233334 6.941666 6.573334 6.885000 0 6.573334 7.168334 C +Wav 0 9.605000 3.258334 9.945000 3.201666 0 9.945000 3.485000 C +Att 0 12.891666 3.343334 13.231666 3.286666 0 13.231666 3.570000 C +Sel 0 15.696663 3.286666 16.036667 3.230000 0 16.036667 3.513334 C +Cs 0 17.765000 7.083334 18.105000 7.026667 0 18.105000 7.310000 C +G9 0.000000 0.000000 1 +T1 1.000000 0 0 1 0 6.205000 5.071666 5.921666 4.873334 6.488334 5.213334 0 + 1 2 0 0 0.000000 0.000000 + 1 + 1 1 0 0 0.000000 0.000000 + 0 +T2 1.000000 0 0 1 1 7.961666 3.230000 7.678334 3.031666 8.245000 3.371666 0 + 1 1 0 0 0.000000 0.000000 + 1 + 1 3 0 0 0.000000 0.000000 + 3 + 1 4 1 0 0.000000 0.000000 +10.171666 4.391666 + 1 6 1 0 0.000000 0.000000 +10.030000 5.355000 + 1 5 2 0 0.000000 0.000000 +10.001666 4.930000 +15.555000 5.666666 +T3 1.000000 0 0 1 1 11.191666 3.315000 10.908334 3.116666 11.475000 3.456666 0 + 1 3 0 0 0.000000 0.000000 + 1 + 1 4 0 0 0.000000 0.000000 + 0 +T4 1.000000 0 0 1 1 14.308334 3.343334 14.025000 3.145000 14.591666 3.485000 0 + 1 4 0 0 0.000000 0.000000 + 1 + 1 5 0 0 0.000000 0.000000 + 1 + 1 5 1 0 0.000000 0.000000 +14.903334 2.635000 +T6 1.000000 0 0 1 1 17.680001 3.286666 17.396666 3.088334 17.963334 3.428334 0 + 1 5 0 0 0.000000 0.000000 + 1 + 1 6 0 0 0.000000 0.000000 + 2 + 1 3 1 0 0.000000 0.000000 +14.223334 1.983334 + 1 6 1 0 0.000000 0.000000 +17.056667 5.241666 +T7 1.000000 0 0 1 1 12.126666 6.941666 11.843334 6.743334 12.410000 7.083334 0 + 1 6 0 0 0.000000 0.000000 + 1 + 1 2 0 0 0.000000 0.000000 + 0 +t5 1.000000 1 1 2 1 14.336667 4.136666 13.855000 3.626666 14.620001 4.278334 0 14.620001 3.938334 [d(x)=C8 or (d(x)=C7 and (d(y)=C6 or d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C6 and (d(y)=C5 or d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or (d(x)=C5 and (d(y)=C4 or d(y)=C3 or d(y)=C2 or d(y)=C1)) or(d(x)=C4 and (d(y)=C3 or d(y)=C2 or d(y)=C1))or(d(x)=C3 and (d(y)=C2 or d(y)=C1))or(d(x)=C2 and d(y)=C1)] + 1 4 0 0 0.000000 0.000000 + 1 5 1 0 0.000000 0.000000 +15.498334 4.646666 + 2 + 1 4 1 0 0.000000 0.000000 +13.061666 4.561666 + 1 5 0 0 0.000000 0.000000 + 0 diff --git a/bench/gspn-ssp/templates/predef/WCSasym8.tobs b/bench/gspn-ssp/templates/predef/WCSasym8.tobs new file mode 100644 index 000000000..a30336159 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/WCSasym8.tobs @@ -0,0 +1,33 @@ +8 +P1 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 4 0 0 1.000000 1.000000 + 0 + 0 +P2 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 6 0 0 1.000000 1.000000 2 + 0 + 0 +P3 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 +P4 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C1 ] + 1 2 0 0 1.000000 1.000000 2 + 0 + 0 +P5 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 4 0 0 1.000000 1.000000 2 + 0 + 0 +P6 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 + 1 1 0 0 1.000000 1.000000 + + 0 + 0 +P7 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 3 0 0 1.000000 1.000000 + 0 + 0 +P8 1.0 1 0 1 0 1.000000 1.000000 1.000000 1.000000 1.0 1.0 0 1.0 1.0 [d(x)=C2 ] + 1 1 0 0 1.000000 1.000000 + 0 + 0 diff --git a/bench/gspn-ssp/templates/predef/gen b/bench/gspn-ssp/templates/predef/gen new file mode 100755 index 000000000..e12baaad1 --- /dev/null +++ b/bench/gspn-ssp/templates/predef/gen @@ -0,0 +1,9 @@ +#!/bin/sh +for i in 3 4 5 6 8; do + dst=../../models/WCSasym$i.rg + mkdir $dst + for e in def net tobs; do + cp WCSasym$i.$e $dst/WCSasym$i.rg.$e + done + echo 'P1 P2 P3 P4 P5 P6 P7 P8' > $dst/WCSasym$i.rg.ap +done diff --git a/bench/gspn-ssp/trans2prop.pl b/bench/gspn-ssp/trans2prop.pl new file mode 100755 index 000000000..b3c0c4ba3 --- /dev/null +++ b/bench/gspn-ssp/trans2prop.pl @@ -0,0 +1,89 @@ +#!/usr/bin/perl -w + +use strict 'vars'; + +die "Please specify model name as first argument to script.\n" + unless 1 != $#ARGV; + +my $modelname = $ARGV[0]; +#print "Will work on model \"$modelname\"\n"; +my $netf = "$modelname.net"; +my $deff = "$modelname.def"; +my $propf = "$modelname.tobs"; +my $tmpf = "$modelname.nettmp"; +open (NET, "< $netf") or die "cannot open $netf\n"; +open (DEF, "< $deff") or die "cannot open $deff\n"; +open (PROP, "> $propf") or die "cannot open $propf\n"; +open (OUTNET,"> $tmpf") or die "cannot open $tmpf\n"; + + +my %defs = (); +{ + local $/; + my $contents = ; + close DEF; + while ($contents =~ /\((F\d+)\s[^\(]*\(\@f\n(.*)\n\)\)/gom) + { + $defs{$1} = $2; + } +} + +my $line = ; +print OUTNET $line; +$line = ; +print OUTNET $line; + +$line = ; +my @split = split (/\s+/, $line); + +my $nump = $split[2]; +my $numt = $split[4]; + +#print "$nump places, $numt transitions\n"; + +my $places ; +for (my $i = 0; $i < $nump; $i++) + { + $places .= ; + } +my %trans = (); +my $transline = ; +for (my $i = 0; $i < $numt; $i++) + { + my $tname = (split (/ /,$transline))[0]; + $trans{$tname} .= $transline; + $trans{$tname} .= $line while (defined ($line = ) && $line =~ /^\s/); +# print "analyzed transition $tname:\n$trans{$tname}\n"; + $transline = $line; + } + +my $numpt = grep /^PROP\_/, keys %trans; +$split[4] -= $numpt ; + +print OUTNET (join (" ",@split)); +print OUTNET "\n"; +print OUTNET $places; +print PROP "$numpt\n"; +my $props = ''; +foreach my $key (keys %trans) + { + if ($key =~ /^PROP_/) + { + $props .= $trans{$key}; + } + else + { + print OUTNET $trans{$key} + } + } + +$props =~ s/^PROP_//gm; +while (my ($key, $val) = each %defs) + { + $props =~ s/$key\s*$/$val/gm; + } + +close OUTNET; +print PROP $props; +close PROP; +close NET; diff --git a/configure.ac b/configure.ac index 63ed67b65..4126db8d1 100644 --- a/configure.ac +++ b/configure.ac @@ -72,6 +72,8 @@ AC_CONFIG_FILES([ bench/Makefile bench/emptchk/Makefile bench/emptchk/defs + bench/gspn-ssp/Makefile + bench/gspn-ssp/defs bench/ltl2tgba/Makefile bench/ltl2tgba/defs doc/Doxyfile