diff --git a/ChangeLog b/ChangeLog index 443ce7372..431485ee2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-11-24 Alexandre Duret-Lutz + + Fix bench/emptchk/pml2tgba.pl for more recent Spin version. + + * bench/emptchk/pml2tgba.pl: Stop checking for version start lines + depending on the Spin version. This check was never always + correct. Reported by Étienne Renault. + 2011-11-24 Alexandre Duret-Lutz Update formulae.ltl not to use uncommon operators. diff --git a/bench/emptchk/pml2tgba.pl b/bench/emptchk/pml2tgba.pl index 70084390a..27931c507 100755 --- a/bench/emptchk/pml2tgba.pl +++ b/bench/emptchk/pml2tgba.pl @@ -112,15 +112,6 @@ while (1) my $model = shift @ARGV; -# Find out the start of the never claim. -# The line numbering changed in Spin 5.2.0. -my $model_size = `wc -l <"$model"`; -my $neverstartline_spin517 = 3 + $model_size; -my $neverstartline_spin520 = 4 + $model_size; -my $neverstartline_spin525 = 0 + $model_size; -my $neverstartline = - "($neverstartline_spin517|$neverstartline_spin520|$neverstartline_spin525)"; - # Create the automaton open NEVER, ">never.$$"; print NEVER create_2n_automaton (@ARGV); @@ -140,7 +131,7 @@ while () while () { next - unless (/\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.* line $neverstartline =>/o); + unless (/\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.* line \d+ =>/o); # We are assuming that transition are output by -d in the same order # as we specified them in the neverclaim. my $prop = shift @prop_list;