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

* iface/gspn/ltlgspn.cc: Add option -P.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-01-09 10:31:01 +00:00
parent 92cc5f9b9f
commit 4732d165db
2 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2004-01-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/ltlgspn.cc: Add option -P.
2004-01-08 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-01-08 Alexandre Duret-Lutz <adl@src.lip6.fr>
Run valgrind in test cases. Run valgrind in test cases.

17
iface/gspn/ltlgspn.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -35,7 +35,7 @@ syntax(char* prog)
std::cerr << "Usage: "<< prog std::cerr << "Usage: "<< prog
<< " [OPTIONS...] model formula props..." << std::endl << " [OPTIONS...] model formula props..." << std::endl
<< std::endl << std::endl
<< " -c compute a counter example" << std::endl << " -c compute an example" << std::endl
<< " (instead of just checking for emptiness)" << std::endl << " (instead of just checking for emptiness)" << std::endl
<< std::endl << std::endl
<< " -e use Couvreur's emptiness-check (default)" << std::endl << " -e use Couvreur's emptiness-check (default)" << std::endl
@ -43,8 +43,8 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -l use Couvreur's LaCIM algorithm for translation (default)" << " -l use Couvreur's LaCIM algorithm for translation (default)"
<< std::endl << std::endl
<< " -f use Couvreur's FM algorithm for translation" << " -f use Couvreur's FM algorithm for translation" << std::endl
<< std::endl; << " -P do not project example on model" << std::endl;
exit(2); exit(2);
} }
@ -56,6 +56,7 @@ main(int argc, char **argv)
enum { Couvreur, Magic } check = Couvreur; enum { Couvreur, Magic } check = Couvreur;
enum { Lacim, Fm } trans = Lacim; enum { Lacim, Fm } trans = Lacim;
bool compute_counter_example = false; bool compute_counter_example = false;
bool proj = true;
spot::gspn_environment env; spot::gspn_environment env;
@ -81,6 +82,10 @@ main(int argc, char **argv)
{ {
trans = Fm; trans = Fm;
} }
else if (!strcmp(argv[formula_index], "-P"))
{
proj = 0;
}
else else
{ {
syntax(argv[0]); syntax(argv[0]);
@ -135,7 +140,7 @@ main(int argc, char **argv)
if (compute_counter_example) if (compute_counter_example)
{ {
ec.counter_example(); ec.counter_example();
ec.print_result(std::cout, model); ec.print_result(std::cout, proj ? model : 0);
} }
else else
{ {
@ -157,7 +162,7 @@ main(int argc, char **argv)
if (ms.check()) if (ms.check())
{ {
if (compute_counter_example) if (compute_counter_example)
ms.print_result (std::cout, model); ms.print_result (std::cout, proj ? model : 0);
else else
std::cout << "non-empty" << std::endl; std::cout << "non-empty" << std::endl;
exit(1); exit(1);