...
 
Commits (4)
...@@ -68,7 +68,7 @@ namespace spot ...@@ -68,7 +68,7 @@ namespace spot
/// a given parameter is of type kripkecube. It also check /// a given parameter is of type kripkecube. It also check
/// if the iterator has the good interface. /// if the iterator has the good interface.
template <typename T, typename State, typename SuccIter> template <typename T, typename State, typename SuccIter>
class is_a_kripkecube_ptr class SPOT_API is_a_kripkecube_ptr
{ {
private: private:
using yes = std::true_type; using yes = std::true_type;
......
...@@ -36,6 +36,47 @@ ...@@ -36,6 +36,47 @@
namespace spot namespace spot
{ {
/// \brief This class allows to ensure (at compile time) if
/// a given parameter can be compsidered as a modelchecking algorithm
/// (i.e., usable by instanciate)
template <typename T>
class SPOT_API is_a_mc_algorithm
{
private:
using yes = std::true_type;
using no = std::false_type;
// Hardly waiting C++ concepts...
template<typename U> static auto test_mc_algo(U u)
-> decltype(
// Check the kripke
std::is_same<void, decltype(u->setup())>::value &&
std::is_same<void, decltype(u->run())>::value &&
std::is_same<void, decltype(u->finalize())>::value &&
std::is_same<bool, decltype(u->finisher())>::value &&
std::is_same<unsigned, decltype(u->states())>::value &&
std::is_same<unsigned, decltype(u->transitions())>::value &&
std::is_same<unsigned, decltype(u->walltime())>::value &&
std::is_same<std::string, decltype(u->name())>::value &&
std::is_same<int, decltype(u->sccs())>::value &&
std::is_same<mc_rvalue, decltype(u->result())>::value &&
std::is_same<std::string, decltype(u->trace())>::value
// finally return the type "yes"
, yes());
// For all other cases return the type "no"
template<typename> static no test_mc_algo(...);
public:
/// \brief Checking this value will ensure, at compile time, that the
/// Kripke specialisation respects the required interface.
static constexpr bool value =
std::is_same< decltype(test_mc_algo<T>(nullptr)), yes>::value;
};
template<typename algo_name, typename kripke_ptr, typename State, template<typename algo_name, typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal> typename Iterator, typename Hash, typename Equal>
static SPOT_API ec_stats instanciate(kripke_ptr sys, static SPOT_API ec_stats instanciate(kripke_ptr sys,
...@@ -60,6 +101,10 @@ namespace spot ...@@ -60,6 +101,10 @@ namespace spot
{ {
ss[i] = algo_name::make_shared_structure(map, i); ss[i] = algo_name::make_shared_structure(map, i);
swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop); swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop);
static_assert(spot::is_a_mc_algorithm<decltype(&*swarmed[i])>::value,
"error: does not match the kripkecube requirements");
} }
tm.stop("Initialisation"); tm.stop("Initialisation");
......
...@@ -19,6 +19,7 @@ ...@@ -19,6 +19,7 @@
#include "config.h" #include "config.h"
#include <spot/twacube_algos/convert.hh> #include <spot/twacube_algos/convert.hh>
#include <spot/twaalgos/contains.hh>
#include <assert.h> #include <assert.h>
namespace spot namespace spot
...@@ -97,23 +98,17 @@ namespace spot ...@@ -97,23 +98,17 @@ namespace spot
// Special case for bddfalse // Special case for bddfalse
if (cond == bddfalse) if (cond == bddfalse)
continue;
// Split the bdd into multiple transitions
while (cond != bddfalse)
{ {
spot::cube cube = tg->get_cubeset().alloc(); bdd one = bdd_satone(cond);
for (unsigned int i = 0; i < cs.size(); ++i) cond -= one;
cs.set_false_var(cube, i); // FIXME ! use fill! spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, tg->create_transition(st_binder[n], cube, t.acc,
t.acc, st_binder[t.dst]); st_binder[t.dst]);
} }
else
// Split the bdd into multiple transitions
while (cond != bddfalse)
{
bdd one = bdd_satone(cond);
cond -= one;
spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
tg->create_transition(st_binder[n], cube, t.acc,
st_binder[t.dst]);
}
} }
// Must be contiguous to support swarming. // Must be contiguous to support swarming.
assert(tg->succ_contiguous()); assert(tg->succ_contiguous());
...@@ -187,4 +182,76 @@ namespace spot ...@@ -187,4 +182,76 @@ namespace spot
return res; return res;
} }
// FIXME this code is very close to twacube_to_twa, can we merge both?
bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa)
{
// Compute the necessary binder and extract atomic propositions
std::unordered_map<int, int> ap_binder;
std::vector<std::string>* aps_twa = extract_aps(twa, ap_binder);
std::vector<std::string> aps_twacube = twacube->ap();
// Comparator to compare two strings in case insensitive manner
std::function< bool (const std::string&, const std::string&) >
comparator = [](const std::string& lhs, const std::string& rhs){
return lhs.compare(rhs) == 0;
};
// Error. Not working on the same set of aps.
if (aps_twa->size() != aps_twacube.size() ||
!std::equal(aps_twa->begin(), aps_twa->end(),
aps_twacube.begin(), comparator))
throw std::runtime_error("are_equivalent: not working on the same "
"atomic propositions");
// Grab necessary variables
auto& theg = twacube->get_graph();
spot::cubeset cs = twacube->get_cubeset();
auto d = twa->get_dict();
auto res = make_twa_graph(d);
// Fix the acceptance of the resulting automaton
res->acc() = twacube->acc();
// Grep bdd id for each atomic propositions
std::vector<int> bdds_ref;
for (unsigned i = 0; i < aps_twacube.size(); ++i)
{
bdds_ref.push_back(ap_binder[i]);
}
// Build all resulting states
for (unsigned int i = 0; i < theg.num_states(); ++i)
{
unsigned st = res->new_state();
(void) st;
assert(st == i);
}
// Build all resulting conditions.
for (unsigned int i = 1; i <= theg.num_edges(); ++i)
{
bdd cond = bddtrue;
for (unsigned j = 0; j < cs.size(); ++j)
{
if (cs.is_true_var(theg.edge_data(i).cube_, j))
cond &= bdd_ithvar(bdds_ref[j]);
else if (cs.is_false_var(theg.edge_data(i).cube_, j))
cond &= bdd_nithvar(bdds_ref[j]);
// otherwise it 's a free variable do nothing
}
res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
cond, theg.edge_data(i).acc_);
}
// Fix the initial state
res->set_init_state(twacube->get_initial());
bool result = are_equivalent(res, twa);
delete aps_twa;
return result;
}
} }
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement de // Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -53,4 +53,8 @@ namespace spot ...@@ -53,4 +53,8 @@ namespace spot
/// \brief Convert a twacube into a twa /// \brief Convert a twacube into a twa
SPOT_API spot::twa_graph_ptr SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube); twacube_to_twa(spot::twacube_ptr twacube);
/// \brief Check wether a twacube and a twa are equivalent
SPOT_API bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa);
} }
...@@ -49,6 +49,8 @@ int main() ...@@ -49,6 +49,8 @@ int main()
// Test translation // Test translation
auto aut = twa_to_twacube(tg); auto aut = twa_to_twacube(tg);
assert(spot::are_equivalent(aut, tg));
spot::print_dot(std::cout, tg, "A"); spot::print_dot(std::cout, tg, "A");
std::cout << "-----------\n" << *aut << "-----------\n"; std::cout << "-----------\n" << *aut << "-----------\n";
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016, 2018 Laboratoire de Recherche et # Copyright (C) 2014, 2015, 2016, 2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -51,7 +51,6 @@ digraph "" { ...@@ -51,7 +51,6 @@ digraph "" {
} }
----------- -----------
init : 0 init : 0
0->0 : !p1&!p2 {}
0->1 : p1 {} 0->1 : p1 {}
0->2 : p2 {1} 0->2 : p2 {1}
1->2 : p1&p2 {0} 1->2 : p1&p2 {0}
...@@ -72,7 +71,6 @@ digraph "" { ...@@ -72,7 +71,6 @@ digraph "" {
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> 0 I -> 0
0 [label="0"] 0 [label="0"]
0 -> 0 [label="!p1 & !p2"]
0 -> 1 [label="p1"] 0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"] 0 -> 2 [label="p2\n{1}"]
1 [label="1"] 1 [label="1"]
......