From 71d1a4fe2563941c068c23bc2fdcde4b33fc714e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 Nov 2011 22:07:09 +0100 Subject: [PATCH] Fix bench/emptchk/pml2tgba.pl for more recent Spin version. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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. --- ChangeLog | 8 ++++++++ bench/emptchk/pml2tgba.pl | 11 +---------- 2 files changed, 9 insertions(+), 10 deletions(-) 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;