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

* src/tgbatest/ltl2tgba.cc: Add option -P.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-12-14 18:40:57 +00:00
parent 60f50d66e0
commit 73c42db23d
2 changed files with 27 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2004-12-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/ltl2tgba.cc: Add option -P.
2004-12-14 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr> 2004-12-14 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbaalgos/ndfs_result.hh: Define the trace output stream. * src/tgbaalgos/ndfs_result.hh: Define the trace output stream.

27
src/tgbatest/ltl2tgba.cc
View file

@ -35,6 +35,7 @@
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh" #include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gv04.hh" #include "tgbaalgos/gv04.hh"
#include "tgbaalgos/magic.hh" #include "tgbaalgos/magic.hh"
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
@ -82,6 +83,8 @@ syntax(char* prog)
<< " -N display the never clain for Spin " << " -N display the never clain for Spin "
<< "(implies -D)" << std::endl << "(implies -D)" << std::endl
<< " -p branching postponement (implies -f)" << std::endl << " -p branching postponement (implies -f)" << std::endl
<< " -Pfile multiply the formula with the automaton from `file'."
<< std::endl
<< " -r display the relation BDD, not the reachability graph" << " -r display the relation BDD, not the reachability graph"
<< std::endl << std::endl
<< " -r1 reduce formula using basic rewriting" << std::endl << " -r1 reduce formula using basic rewriting" << std::endl
@ -178,6 +181,9 @@ main(int argc, char** argv)
bool opt_reduce = false; bool opt_reduce = false;
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* unobservables = 0; spot::ltl::atomic_prop_set* unobservables = 0;
spot::tgba_explicit* system = 0;
spot::tgba* product = 0;
spot::bdd_dict* dict = new spot::bdd_dict();
for (;;) for (;;)
{ {
@ -269,6 +275,16 @@ main(int argc, char** argv)
post_branching = true; post_branching = true;
fm_opt = true; fm_opt = true;
} }
else if (!strncmp(argv[formula_index], "-P", 2))
{
spot::tgba_parse_error_list pel;
system = spot::tgba_parse(argv[formula_index] + 2,
pel, dict, env, debug_opt);
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
system->merge_transitions();
std::clog << argv[formula_index] + 2 << " read" << std::endl;
}
else if (!strcmp(argv[formula_index], "-r")) else if (!strcmp(argv[formula_index], "-r"))
{ {
output = 1; output = 1;
@ -458,8 +474,8 @@ main(int argc, char** argv)
} }
} }
if ((graph_run_opt || graph_run_tgba_opt) && if ((graph_run_opt || graph_run_tgba_opt)
(echeck_algo == "" || !expect_counter_example)) && (echeck_algo == "" || !expect_counter_example))
{ {
std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl; std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
exit(1); exit(1);
@ -494,8 +510,6 @@ main(int argc, char** argv)
input = argv[formula_index]; input = argv[formula_index];
} }
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::formula* f = 0; spot::ltl::formula* f = 0;
if (!from_file) if (!from_file)
{ {
@ -619,6 +633,9 @@ main(int argc, char** argv)
break; break;
} }
if (system)
a = product = new spot::tgba_product(system, a);
switch (output) switch (output)
{ {
case -1: case -1:
@ -785,6 +802,8 @@ main(int argc, char** argv)
if (f) if (f)
spot::ltl::destroy(f); spot::ltl::destroy(f);
delete product;
delete system;
delete expl; delete expl;
delete degeneralized; delete degeneralized;
delete aut_red; delete aut_red;