From 8880578e0dd28194474f26adac095cc5e30630c7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Feb 2016 22:07:21 +0100 Subject: [PATCH] * bench/emptchk/pml2tgba.pl: Fix to work with recent Spin. --- bench/emptchk/pml2tgba.pl | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/bench/emptchk/pml2tgba.pl b/bench/emptchk/pml2tgba.pl index 61f5e0565..159f718d3 100755 --- a/bench/emptchk/pml2tgba.pl +++ b/bench/emptchk/pml2tgba.pl @@ -115,8 +115,12 @@ open NEVER, ">never.$$"; print NEVER create_2n_automaton (@ARGV); close NEVER; -system "spin -a -N never.$$ \"$model\""; -unlink "never.$$"; +# Make a local copy of the model. Recent versions of Spin (at least +# 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"; # Match Büchi states to propositions @@ -124,12 +128,12 @@ my $buechitrans = 'BUG'; open PAN, "./pan -d|"; while () { - last if /^proctype :never/; + last if /^proctype :never/ || /^claim never/; } while () { 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 # as we specified them in the neverclaim. my $prop = shift @prop_list;