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

* bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2005-02-01 16:52:22 +00:00
parent ce871f2f2e
commit 461fcd3732
2 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
ChangeLog
View file

@ -1,5 +1,7 @@
2005-02-01 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-02-01 Alexandre Duret-Lutz <adl@src.lip6.fr>
* bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis.
* bench/emptchk/README: Timing info from Denis. * bench/emptchk/README: Timing info from Denis.
* src/tgbatest/randtgba.cc (main): Skip empty lines. * src/tgbatest/randtgba.cc (main): Skip empty lines.

8
bench/emptchk/pml2tgba.pl
View file

@ -1,6 +1,6 @@
#!/usr/bin/perl -w #!/usr/bin/perl -w
# #
# Copyright (C) 2004 Stefan Schwoon # Copyright (C) 2004 Stefan Schwoon
# #
# This program is free software; you can redistribute it and/or modify # This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by # it under the terms of the GNU General Public License as published by
@ -17,7 +17,7 @@
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA # Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA
# #
# #
# This script was originally distributed by Schwoon alongside with # This script was originally distributed by Schwoon alongside
# #
# @InProceedings{ schwoon.05.tacas, # @InProceedings{ schwoon.05.tacas,
# author = {Stefan Schwoon and Javier Esparza}, # author = {Stefan Schwoon and Javier Esparza},
@ -45,8 +45,8 @@ my %props;
sub usage() sub usage()
{ {
print <<EOF; print <<EOF;
Usage: pan2tgba.pl [-w] promela-model properties... Usage: pml2tgba.pl [-w] promela-model properties...
Extracts the product state space of the model, observing properties. Extract the state-space of the promela-model, observing properties.
If -w is given, output acceptance conditions to ensure weak fairness. If -w is given, output acceptance conditions to ensure weak fairness.
EOF EOF
exit 1; exit 1;