export a create_atomic_prop_set() function
* src/ltlvisit/apcollect.hh, src/ltlvisit/apcollect.cc (create_atomic_prop_set): New function. * src/bin/randltl.cc, bench/stutter/stutter_invariance_randomgraph.cc: Use it.
This commit is contained in:
parent
f08a26f7b9
commit
0250a32747
4 changed files with 24 additions and 24 deletions
|
|
@ -18,7 +18,7 @@
|
||||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
#include "misc/timer.hh"
|
#include "misc/timer.hh"
|
||||||
#include "ltlast/atomic_prop.hh"
|
#include "ltlvisit/apcollect.hh"
|
||||||
#include "tgbaalgos/dtgbacomp.hh"
|
#include "tgbaalgos/dtgbacomp.hh"
|
||||||
#include "tgbaalgos/stutter_invariance.hh"
|
#include "tgbaalgos/stutter_invariance.hh"
|
||||||
#include "tgbaalgos/randomgraph.hh"
|
#include "tgbaalgos/randomgraph.hh"
|
||||||
|
|
@ -45,20 +45,11 @@ main()
|
||||||
for (unsigned props_n = 1; props_n <= 4; ++props_n)
|
for (unsigned props_n = 1; props_n <= 4; ++props_n)
|
||||||
{
|
{
|
||||||
// random ap set
|
// random ap set
|
||||||
auto ap = new spot::ltl::atomic_prop_set();
|
auto ap = spot::ltl::create_atomic_prop_set(props_n);
|
||||||
spot::ltl::default_environment& e =
|
|
||||||
spot::ltl::default_environment::instance();
|
|
||||||
for (unsigned i = 1; i < props_n; ++i)
|
|
||||||
{
|
|
||||||
std::ostringstream p;
|
|
||||||
p << 'p' << i;
|
|
||||||
ap->insert(static_cast<const spot::ltl::atomic_prop*>
|
|
||||||
(e.require(p.str())));
|
|
||||||
}
|
|
||||||
|
|
||||||
// ap set as bdd
|
// ap set as bdd
|
||||||
bdd apdict = bddtrue;
|
bdd apdict = bddtrue;
|
||||||
for (auto& i: *ap)
|
for (auto& i: ap)
|
||||||
apdict &= bdd_ithvar(dict->register_proposition(i, a));
|
apdict &= bdd_ithvar(dict->register_proposition(i, a));
|
||||||
|
|
||||||
// generate n random automata
|
// generate n random automata
|
||||||
|
|
@ -67,7 +58,7 @@ main()
|
||||||
std::vector<aut_pair_t> vec;
|
std::vector<aut_pair_t> vec;
|
||||||
for (unsigned i = 0; i < n; ++i)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
{
|
{
|
||||||
a = spot::random_graph(states_n, d, ap, dict, 2, 0.1, 0.5,
|
a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5,
|
||||||
true);
|
true);
|
||||||
na = spot::dtgba_complement(a);
|
na = spot::dtgba_complement(a);
|
||||||
vec.push_back(aut_pair_t(a, na));
|
vec.push_back(aut_pair_t(a, na));
|
||||||
|
|
@ -94,8 +85,7 @@ main()
|
||||||
std::cout << algo << ", " << props_n << ", " << states_n
|
std::cout << algo << ", " << props_n << ", " << states_n
|
||||||
<< ", " << res << ", " << time << std::endl;
|
<< ", " << res << ", " << time << std::endl;
|
||||||
}
|
}
|
||||||
spot::ltl::destroy_atomic_prop_set(*ap);
|
spot::ltl::destroy_atomic_prop_set(ap);
|
||||||
delete ap;
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -256,15 +256,7 @@ parse_opt(int key, char* arg, struct argp_state* as)
|
||||||
if (!*endptr && res >= 0) // arg is a number
|
if (!*endptr && res >= 0) // arg is a number
|
||||||
{
|
{
|
||||||
ap_count_given = true;
|
ap_count_given = true;
|
||||||
spot::ltl::default_environment& e =
|
aprops = spot::ltl::create_atomic_prop_set(res);
|
||||||
spot::ltl::default_environment::instance();
|
|
||||||
for (int i = 0; i < res; ++i)
|
|
||||||
{
|
|
||||||
std::ostringstream p;
|
|
||||||
p << 'p' << i;
|
|
||||||
aprops.insert(static_cast<const spot::ltl::atomic_prop*>
|
|
||||||
(e.require(p.str())));
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -53,6 +53,20 @@ namespace spot
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
atomic_prop_set create_atomic_prop_set(unsigned n)
|
||||||
|
{
|
||||||
|
atomic_prop_set res;
|
||||||
|
auto& e = spot::ltl::default_environment::instance();
|
||||||
|
for (unsigned i = 0; i < n; ++i)
|
||||||
|
{
|
||||||
|
std::ostringstream p;
|
||||||
|
p << 'p' << i;
|
||||||
|
res.insert(static_cast<const spot::ltl::atomic_prop*>
|
||||||
|
(e.require(p.str())));
|
||||||
|
}
|
||||||
|
return res;
|
||||||
|
}
|
||||||
|
|
||||||
void destroy_atomic_prop_set(atomic_prop_set& aprops)
|
void destroy_atomic_prop_set(atomic_prop_set& aprops)
|
||||||
{
|
{
|
||||||
atomic_prop_set::const_iterator i = aprops.begin();
|
atomic_prop_set::const_iterator i = aprops.begin();
|
||||||
|
|
|
||||||
|
|
@ -39,6 +39,10 @@ namespace spot
|
||||||
typedef std::set<const atomic_prop*,
|
typedef std::set<const atomic_prop*,
|
||||||
formula_ptr_less_than> atomic_prop_set;
|
formula_ptr_less_than> atomic_prop_set;
|
||||||
|
|
||||||
|
/// \brief construct an atomic_prop_set with n propositions
|
||||||
|
SPOT_API
|
||||||
|
atomic_prop_set create_atomic_prop_set(unsigned n);
|
||||||
|
|
||||||
/// \brief Destroy all the atomic propositions in an
|
/// \brief Destroy all the atomic propositions in an
|
||||||
/// atomic_prop_set.
|
/// atomic_prop_set.
|
||||||
SPOT_API void
|
SPOT_API void
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue