alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* bench/emptchk/pml2tgba.pl: Fix to work with recent Spin.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2016-02-03 22:07:21 +01:00
parent 22345d0c67
commit 8880578e0d
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

12
bench/emptchk/pml2tgba.pl
View file

@ -115,8 +115,12 @@ open NEVER, ">never.$$";
print NEVER create_2n_automaton (@ARGV); print NEVER create_2n_automaton (@ARGV);
close NEVER; close NEVER;
system "spin -a -N never.$$ \"$model\""; # Make a local copy of the model. Recent versions of Spin (at least
unlink "never.$$"; # Spin 6.4.3) have problem compiling models that are in
# subdirectories; this was not the case in the past.
system "cp \"$model\" model.$$";
system "spin -a -N never.$$ model.$$";
unlink "never.$$", "model.$$";
system "gcc -DCHECK$reduce -O -o pan pan.c 2>/dev/null"; system "gcc -DCHECK$reduce -O -o pan pan.c 2>/dev/null";
# Match Büchi states to propositions # Match Büchi states to propositions
@ -124,12 +128,12 @@ my $buechitrans = 'BUG';
open PAN, "./pan -d|"; open PAN, "./pan -d|";
while (<PAN>) while (<PAN>)
{ {
last if /^proctype :never/; last if /^proctype :never/ || /^claim never/;
} }
while (<PAN>) while (<PAN>)
{ {
next next
unless (/\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.* line \d+ =>/o); unless (/^\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.*\d+ =>/o);
# We are assuming that transition are output by -d in the same order # We are assuming that transition are output by -d in the same order
# as we specified them in the neverclaim. # as we specified them in the neverclaim.
my $prop = shift @prop_list; my $prop = shift @prop_list;