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

Twacube must share the order of atomic propositions

Browse source 
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
tests/ltsmin/modelcheck.cc: here.
This commit is contained in:
Etienne Renault 2016-09-28 16:31:01 +02:00
parent a1787dd1ce
commit 50d888adf8
3 changed files with 24 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

32
spot/ltsmin/ltsmin.cc
View file

@ -45,6 +45,9 @@
#include <spot/mc/ec.hh>
#include <bricks/brick-hashset.h>
#include <bricks/brick-hash.h>
#include <spot/twaalgos/dot.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/emptiness.hh>
using namespace std::string_literals;
@ -1706,13 +1709,13 @@ namespace spot
relop oper;
// Now, left and (possibly) right are should refer atomic
// Now, left and (possibly) right may refer atomic
// propositions or specific state inside of a process.
// First check if it is a known atomic proposition
it = std::find(k_aps.begin(), k_aps.end(), left);
if (it != k_aps.end())
{
// The aps is directly an AP of the system, we will just
// The ap is directly an AP of the system, we will just
// have to detect if the variable is 0 or not.
lval = std::distance(k_aps.begin(), it);
}
@ -1939,7 +1942,7 @@ namespace spot
}
ltsmin_kripkecube_ptr
ltsmin_model::kripkecube(const atomic_prop_set* to_observe,
ltsmin_model::kripkecube(std::vector<std::string> to_observe,
const formula dead, int compress) const
{
// Register the "dead" proposition. There are three cases to
@ -1958,26 +1961,19 @@ namespace spot
else if (dead != spot::formula::tt())
dead_ap = dead.ap_name();
// Build the set of observed propositons, i.e. those in the
// formula
std::vector<std::string> observed;
// Is dead proposition is already in to_observe?
bool add_dead = true;
for (auto it: *to_observe)
{
observed.push_back(it.ap_name());
// Dead proposition is already in observed prop
if (it.ap_name().compare(dead_ap))
for (auto it: to_observe)
if (it.compare(dead_ap))
add_dead = false;
}
if (dead_ap.compare("") != 0 && add_dead)
observed.push_back(dead_ap);
to_observe.push_back(dead_ap);
// Finally build the system.
return std::make_shared<spot::kripkecube<spot::cspins_state,
spot::cspins_iterator>>
(iface, compress, observed, selfloopize, dead_ap);
(iface, compress, to_observe, selfloopize, dead_ap);
}
kripke_ptr
@ -2016,6 +2012,12 @@ namespace spot
ltsmin_model::modelcheck(ltsmin_kripkecube_ptr sys,
spot::twacube_ptr twa, bool compute_ctrx)
{
// Must ensure that the two automata are working on the same
// set of atomic propositions.
assert(sys->get_ap().size() == twa->get_ap().size());
for (unsigned int i = 0; i < sys->get_ap().size(); ++i)
assert(sys->get_ap()[i].compare(twa->get_ap()[i]) == 0);
ec_renault13lpar<cspins_state, cspins_iterator,
cspins_state_hash, cspins_state_equal> ec(*sys, twa);
bool has_ctrx = ec.run();

3
spot/ltsmin/ltsmin.hh
View file

@ -83,8 +83,7 @@ namespace spot
// \brief The same as above but returns a kripkecube, i.e. a kripke
// that can be use in parallel. Moreover, it support more ellaborated
// atomic propositions such as "P.a == P.c"
ltsmin_kripkecube_ptr
kripkecube(const atomic_prop_set* to_observe,
ltsmin_kripkecube_ptr kripkecube(std::vector<std::string> to_observe,
formula dead = formula::tt(),
int compress = 0) const;

3
tests/ltsmin/modelcheck.cc
View file

@ -29,6 +29,7 @@
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/memusage.hh>
@ -409,7 +410,7 @@ static int checked_main()
try
{
modelcube = spot::ltsmin_model::load(mc_options.model)
.kripkecube(&ap, deadf, mc_options.compress);
.kripkecube(propcube->get_ap(), deadf, mc_options.compress);
}
catch (std::runtime_error& e)
{