Commit 50b69942 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgba/succiterconcrete.hh

(tgba_succ_iterator_concrete::current_acc_): New attribute.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Set current_acc_.
(tgba_succ_iterator_concrete::current_accepting_conditions):
Simply return it.
parent 24427ccc
2003-07-07 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-07 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::current_acc_): New attribute.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Set current_acc_.
(tgba_succ_iterator_concrete::current_accepting_conditions):
Simply return it.
* configure.ac: Output iface/Makefile and iface/gspn/Makefile. * configure.ac: Output iface/Makefile and iface/gspn/Makefile.
* iface/Makefile.am, iface/gspn/Makefile.am: New files. * iface/Makefile.am, iface/gspn/Makefile.am: New files.
* Makefile.am (SUBDIRS): Add iface. * Makefile.am (SUBDIRS): Add iface.
......
...@@ -99,13 +99,17 @@ namespace spot ...@@ -99,13 +99,17 @@ namespace spot
// cube = (!ab & Acc[a]) // cube = (!ab & Acc[a])
bdd prop = bdd_exist(cube, data_.acc_set); bdd prop = bdd_exist(cube, data_.acc_set);
// prop = (!a)&b // prop = (!a)&b
bdd acc = bdd_forall(bdd_restrict(as, prop), data_.var_set); current_acc_ = bdd_forall(bdd_restrict(as, prop), data_.var_set);
// acc = (Acc[a] | Acc[b]) // acc = (Acc[a] | Acc[b])
bdd all = as & acc; bdd all = as & current_acc_;
// all = (a | (!a)&b) & (Acc[a] | Acc[b]) // all = (a | (!a)&b) & (Acc[a] | Acc[b])
current_ = bdd_exist(all, data_.acc_set) & dest; current_ = bdd_exist(all, data_.acc_set) & dest;
// current_ = (a | (!a)&b) & (Next...) // current_ = (a | (!a)&b) & (Next...)
} }
else
{
current_acc_ = bddfalse;
}
assert(current_ != bddfalse); assert(current_ != bddfalse);
// The destination state, computed here, should be compatible // The destination state, computed here, should be compatible
...@@ -142,10 +146,7 @@ namespace spot ...@@ -142,10 +146,7 @@ namespace spot
tgba_succ_iterator_concrete::current_accepting_conditions() tgba_succ_iterator_concrete::current_accepting_conditions()
{ {
assert(!done()); assert(!done());
return bdd_exist(bdd_forall(bdd_restrict(data_.accepting_conditions, return current_acc_;
current_),
data_.var_set),
data_.notacc_set);
} }
} }
...@@ -42,6 +42,8 @@ namespace spot ...@@ -42,6 +42,8 @@ namespace spot
/// atomic proposition and Next variables. /// atomic proposition and Next variables.
bdd current_state_; ///< \brief Current successor, as a bdd current_state_; ///< \brief Current successor, as a
/// conjunction of Now variables. /// conjunction of Now variables.
bdd current_acc_; ///< \brief Accepting condition for the current
/// transition.
}; };
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment