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

dve2: use the new translator class

Browse source 
* iface/dve2/dve2check.cc: Adjust.
* iface/dve2/README: Some (unrelated) typos.
This commit is contained in:
Alexandre Duret-Lutz 2013-03-26 17:00:44 +01:00
parent c5b7e8e1da
commit 9723738404
2 changed files with 15 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

8
iface/dve2/README
View file

@ -53,8 +53,8 @@ Usage with Spot
The function load_dve2() defined in dve2.hh in this directory The function load_dve2() defined in dve2.hh in this directory
will accept "model.dve" or "model.dve2C" as file argument. will accept "model.dve" or "model.dve2C" as file argument.
In the former case, it will call "divine compile --ltsmin" In the former case, it will call "divine compile --ltsmin"
if "model.dve2C" does not exist or is older. Then load if "model.dve2C" does not exist or is older. Then it will
"model.dve2C" dynamically. load "model.dve2C" dynamically.
load_dve2() also requires a set of atomic propositions that should load_dve2() also requires a set of atomic propositions that should
be observed in the model. These are usually the atomic propositions be observed in the model. These are usually the atomic propositions
@ -100,7 +100,9 @@ Usage with Spot
be enclosed in double quote. be enclosed in double quote.
Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are
considered to be two atomic propositions with the same semantics. considered to be two distinct atomic propositions with the same
semantics.
Examples Examples
======== ========

32
iface/dve2/dve2check.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de // Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
// l'Epita (LRDE) // Developpement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -21,7 +21,7 @@
#include "ltlenv/defaultenv.hh" #include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlparse/public.hh" #include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/translate.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/postproc.hh" #include "tgbaalgos/postproc.hh"
@ -203,15 +203,15 @@ main(int argc, char **argv)
if (exit_code) if (exit_code)
goto safe_exit; goto safe_exit;
tm.start("reducing formula"); tm.start("translating formula");
{ {
spot::ltl::ltl_simplifier_options opt(true, true, true, true, true); spot::translator trans(dict);
spot::ltl::ltl_simplifier simp(opt); if (deterministic)
const spot::ltl::formula* r = simp.simplify(f); trans.set_pref(spot::postprocessor::Deterministic);
f->destroy();
f = r; prop = trans.run(&f);
} }
tm.stop("reducing formula"); tm.stop("translating formula");
atomic_prop_collect(f, &ap); atomic_prop_collect(f, &ap);
@ -243,18 +243,6 @@ main(int argc, char **argv)
} }
} }
tm.start("translating formula");
prop = spot::ltl_to_tgba_fm(f, dict);
tm.stop("translating formula");
if (deterministic)
post.set_pref(spot::postprocessor::Deterministic);
tm.start("postprocessing A_f");
prop = post.run(prop, f);
tm.stop("postprocessing A_f");
if (output == DotFormula) if (output == DotFormula)
{ {
tm.start("dotty output"); tm.start("dotty output");