Commit 1337c9c3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

simulation: many fixes.

* src/tgbaalgos/simulation.cc: Attempt to fix several cases.
* src/tgbatest/sim.test: Add more tests.
* src/tgbatest/sim2.test: New file.
* src/tgbatest/Makefile.am: Add it.
parent a965af71
...@@ -402,7 +402,7 @@ namespace spot ...@@ -402,7 +402,7 @@ namespace spot
// Contains the relation between the names of the states in // Contains the relation between the names of the states in
// the automaton returned by the complementation and the one // the automaton returned by the complementation and the one
// get in argument to the constructor of acc_compl. // get in argument to the constructor of acc_compl.
old_name_ = acc_compl.old_name_; std::swap(old_name_, acc_compl.old_name_);
a_ = acc_compl.out_; a_ = acc_compl.out_;
...@@ -450,7 +450,7 @@ namespace spot ...@@ -450,7 +450,7 @@ namespace spot
relation_[init] = init; relation_[init] = init;
order_ = acc_compl.order_; std::swap(order_, acc_compl.order_);
all_acceptance_conditions_ = a_->all_acceptance_conditions(); all_acceptance_conditions_ = a_->all_acceptance_conditions();
} }
...@@ -1077,8 +1077,11 @@ namespace spot ...@@ -1077,8 +1077,11 @@ namespace spot
bool could_imply(bdd left, bdd left_class, bool could_imply(bdd left, bdd left_class,
bdd right, bdd right_class) bdd right, bdd right_class)
{ {
bdd f1 = bdd_restrict(left, on_cycle_); bdd f1 = bdd_relprod(left, on_cycle_, on_cycle_);
bdd g1 = bdd_restrict(left, !on_cycle_); bdd g1 = bdd_relprod(left, !on_cycle_, on_cycle_);
//bdd f1 = bdd_restrict(left, on_cycle_);
//bdd g1 = bdd_restrict(left, !on_cycle_);
return could_imply_aux(f1, g1, left_class, return could_imply_aux(f1, g1, left_class,
right, right_class); right, right_class);
} }
...@@ -1099,8 +1102,11 @@ namespace spot ...@@ -1099,8 +1102,11 @@ namespace spot
{ {
bdd accu = it1->second; bdd accu = it1->second;
bdd f1 = bdd_restrict(it1->first, on_cycle_); bdd f1 = bdd_relprod(it1->first, on_cycle_, on_cycle_);
bdd g1 = bdd_restrict(it1->first, !on_cycle_); bdd g1 = bdd_relprod(it1->first, !on_cycle_, on_cycle_);
// bdd f1 = bdd_restrict(it1->first_, on_cycle_);
// bdd g1 = bdd_restrict(it1->first_, !on_cycle_);
for (list_bdd_bdd::const_iterator it2 = now_to_next.begin(); for (list_bdd_bdd::const_iterator it2 = now_to_next.begin();
it2 != now_to_next.end(); it2 != now_to_next.end();
...@@ -1125,7 +1131,8 @@ namespace spot ...@@ -1125,7 +1131,8 @@ namespace spot
inline bool is_out_scc(bdd b) inline bool is_out_scc(bdd b)
{ {
return bddfalse != bdd_restrict(b, !on_cycle_); return bddfalse != bdd_relprod(b, !on_cycle_, on_cycle_);
// return bddfalse != bdd_restrict(b, !on_cycle_);
} }
#define create_cstr(src, dst, constraint) \ #define create_cstr(src, dst, constraint) \
...@@ -1143,6 +1150,7 @@ namespace spot ...@@ -1143,6 +1150,7 @@ namespace spot
const state* src_right, const state* src_right,
std::list<constraint>& constraint) std::list<constraint>& constraint)
{ {
assert(src_left != src_right);
// Determine which is the current case. // Determine which is the current case.
bool out_scc_left = is_out_scc(left); bool out_scc_left = is_out_scc(left);
bool out_scc_right = is_out_scc(right); bool out_scc_right = is_out_scc(right);
...@@ -1152,9 +1160,12 @@ namespace spot ...@@ -1152,9 +1160,12 @@ namespace spot
dest_class = bdd_existcomp(right, all_class_var_); dest_class = bdd_existcomp(right, all_class_var_);
const state* dst_right = revert_relation_[dest_class]; const state* dst_right = revert_relation_[dest_class];
assert(src_left != dst_left || src_right != dst_right);
left = bdd_exist(left, all_class_var_ & on_cycle_); left = bdd_exist(left, all_class_var_ & on_cycle_);
right = bdd_exist(right, all_class_var_ & on_cycle_); right = bdd_exist(right, all_class_var_ & on_cycle_);
if (!out_scc_left && out_scc_right) if (!out_scc_left && out_scc_right)
{ {
bdd b = bdd_exist(right, notap); bdd b = bdd_exist(right, notap);
...@@ -1163,6 +1174,8 @@ namespace spot ...@@ -1163,6 +1174,8 @@ namespace spot
if (add != bddfalse if (add != bddfalse
&& bdd_exist(add, all_acceptance_conditions_) == bddtrue) && bdd_exist(add, all_acceptance_conditions_) == bddtrue)
{ {
assert(src_right != dst_right);
constraint constraint
.push_back(create_cstr(new_original_[old_name_[src_right]], .push_back(create_cstr(new_original_[old_name_[src_right]],
new_original_[old_name_[dst_right]], new_original_[old_name_[dst_right]],
...@@ -1177,6 +1190,8 @@ namespace spot ...@@ -1177,6 +1190,8 @@ namespace spot
if (add != bddfalse if (add != bddfalse
&& bdd_exist(add, all_acceptance_conditions_) == bddtrue) && bdd_exist(add, all_acceptance_conditions_) == bddtrue)
{ {
assert(src_left != dst_left);
constraint constraint
.push_back(create_cstr(new_original_[old_name_[src_left]], .push_back(create_cstr(new_original_[old_name_[src_left]],
new_original_[old_name_[dst_left]], new_original_[old_name_[dst_left]],
...@@ -1191,6 +1206,7 @@ namespace spot ...@@ -1191,6 +1206,7 @@ namespace spot
if (add != bddfalse if (add != bddfalse
&& bdd_exist(add, all_acceptance_conditions_) == bddtrue) && bdd_exist(add, all_acceptance_conditions_) == bddtrue)
{ {
assert(src_left != dst_left && src_right != dst_right);
// FIXME: cas pas compris. // FIXME: cas pas compris.
constraint constraint
.push_back(create_cstr(new_original_[old_name_[src_left]], .push_back(create_cstr(new_original_[old_name_[src_left]],
...@@ -1220,42 +1236,69 @@ namespace spot ...@@ -1220,42 +1236,69 @@ namespace spot
const state* right, const state* right,
map_state_bdd& state2sig) map_state_bdd& state2sig)
{ {
bdd pcl = previous_class_[left];
bdd pcr = previous_class_[right];
bdd sigl = state2sig[left]; bdd sigl = state2sig[left];
bdd sigr = state2sig[right]; bdd sigr = state2sig[right];
std::list<constraint> res; std::list<constraint> res;
bdd ex = all_class_var_ & on_cycle_;
bdd both = pcl & pcr;
int lc = bdd_var(pcl);
#define DEST(x) bdd_compose(bdd_existcomp(x, ex), both, lc)
// Key is destination class, value is the signature part that // Key is destination class, value is the signature part that
// led to this destination class. // led to this destination class.
map_bdd_bdd sigl_map; map_bdd_bdd sigl_map;
minato_isop isop(sigl); {
minato_isop isop(sigl & on_cycle_);
bdd cond_acc_dest; bdd cond_acc_dest;
while ((cond_acc_dest = isop.next()) != bddfalse) while ((cond_acc_dest = isop.next()) != bddfalse)
sigl_map[bdd_existcomp(cond_acc_dest, all_class_var_)] sigl_map[DEST(cond_acc_dest)]
|= cond_acc_dest; |= cond_acc_dest;
}
{
minato_isop isop(sigl & !on_cycle_);
bdd cond_acc_dest;
while ((cond_acc_dest = isop.next()) != bddfalse)
sigl_map[DEST(cond_acc_dest)]
|= cond_acc_dest;
}
map_bdd_bdd sigr_map; map_bdd_bdd sigr_map;
minato_isop isop2(sigr); {
minato_isop isop2(sigr & on_cycle_);
bdd cond_acc_dest2; bdd cond_acc_dest2;
while ((cond_acc_dest2 = isop2.next()) != bddfalse) while ((cond_acc_dest2 = isop2.next()) != bddfalse)
sigr_map[bdd_existcomp(cond_acc_dest2, all_class_var_)] sigr_map[DEST(cond_acc_dest2)]
|= cond_acc_dest2; |= cond_acc_dest2;
}
{
minato_isop isop2(sigr & !on_cycle_);
bdd cond_acc_dest2;
while ((cond_acc_dest2 = isop2.next()) != bddfalse)
sigr_map[DEST(cond_acc_dest2)]
|= cond_acc_dest2;
}
// Iterate over the transitions of both states. // Iterate over the transitions of both states.
for (map_bdd_bdd::const_iterator lit = sigl_map.begin(); for (map_bdd_bdd::const_iterator lit = sigl_map.begin();
lit != sigl_map.end(); ++lit) lit != sigl_map.end(); ++lit)
for (map_bdd_bdd::iterator rit = sigr_map.begin(); for (map_bdd_bdd::iterator rit = sigr_map.begin();
rit != sigr_map.end(); ++rit) rit != sigr_map.end(); ++rit)
{
// And create constraints if any of the transitions // And create constraints if any of the transitions
// is out of the SCC and the left could imply the right. // is out of the SCC and the left could imply the right.
if ((is_out_scc(lit->second) || is_out_scc(rit->second)) if ((is_out_scc(lit->second) || is_out_scc(rit->second))
&& could_imply(lit->second, previous_class_[left], && (bdd_exist(lit->first, on_cycle_) ==
rit->second, previous_class_[right])) bdd_exist(rit->first, on_cycle_)))
{ {
create_simple_constraint(lit->second, rit->second, create_simple_constraint(lit->second, rit->second,
left, right, res); left, right, res);
} }
}
return res; return res;
} }
...@@ -1322,7 +1365,7 @@ namespace spot ...@@ -1322,7 +1365,7 @@ namespace spot
// order_ is here for the determinism. Here we make the diff // order_ is here for the determinism. Here we make the diff
// between the two table: imply and could_imply. // between the two tables: imply and could_imply.
for (std::list<const state*>::const_iterator my_it = order_.begin(); for (std::list<const state*>::const_iterator my_it = order_.begin();
my_it != order_.end(); my_it != order_.end();
++my_it) ++my_it)
...@@ -1338,22 +1381,23 @@ namespace spot ...@@ -1338,22 +1381,23 @@ namespace spot
if (care_rel == dont_care_rel) if (care_rel == dont_care_rel)
continue; continue;
// If they are different: We know that dont_care_rel is // If they are different we necessarily have
// '(care_rel | x)' and because it is a conjunction of // dont_care_rel == care_rel & diff
// variable, we can simply use bdd_exist to discover 'x'.
bdd diff = bdd_exist(dont_care_rel, care_rel); bdd diff = bdd_exist(dont_care_rel, care_rel);
assert(dont_care_rel == (care_rel & diff));
assert(diff != bddtrue);
bdd a = diff; do
while (a != bddtrue)
{ {
bdd cur_diff = bdd_ithvar(bdd_var(a)); bdd cur_diff = bdd_ithvar(bdd_var(diff));
cc[it->second][cur_diff] cc[it->second][cur_diff]
= create_new_constraint(it->first, = create_new_constraint(it->first,
class2state[cur_diff], class2state[cur_diff],
dont_care_state2sig); dont_care_state2sig);
++number_constraints; ++number_constraints;
a = bdd_high(a); diff = bdd_high(diff);
} }
while (diff != bddtrue);
} }
#ifndef NDEBUG #ifndef NDEBUG
for (map_bdd_state::const_iterator i = class2state.begin(); for (map_bdd_state::const_iterator i = class2state.begin();
......
...@@ -80,6 +80,7 @@ TESTS = \ ...@@ -80,6 +80,7 @@ TESTS = \
readsave.test \ readsave.test \
simdet.test \ simdet.test \
sim.test \ sim.test \
sim2.test \
ltl2tgba.test \ ltl2tgba.test \
ltl2neverclaim.test \ ltl2neverclaim.test \
ltl2neverclaim-lbtt.test \ ltl2neverclaim-lbtt.test \
......
...@@ -51,12 +51,33 @@ EOF ...@@ -51,12 +51,33 @@ EOF
diff out.tgba expected.tgba diff out.tgba expected.tgba
run 0 ../ltl2tgba -RDCIS -kt 'Fp U Gq' > out.tgba run 0 ../ltl2tgba -RDCIS -kt 'Fp U Gq' > out
cat >expected.tgba <<EOF cat >expected <<EOF
sub trans.: 12 sub trans.: 12
transitions: 6 transitions: 6
states: 3 states: 3
nondeterministic states: 1 nondeterministic states: 1
EOF EOF
diff out.tgba expected.tgba diff out expected
run 0 ../ltl2tgba -R3 -x -RDCS -kt 'F(a & GFa)' > out
run 0 ../ltl2tgba -R3f -x -RDCS -kt 'F(a & GFa)' > out2
diff out out2
f='FG((Fp0 & (!p0 R (F!p1 U !p1))) | (G!p0 & (p0 U (Gp1 R p1))))'
run 0 ../ltl2tgba -R3f -x -RDS -kt "$f" | grep -v sub > out
run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" | grep -v sub > out2
diff out out2
run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" > out2
cat >expected <<EOF
sub trans.: 13
transitions: 8
states: 3
nondeterministic states: 1
EOF
diff out2 expected
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
../ltl2tgba -b -x -R3f -RDS '{(a&b)[*3]}<>=>G(a&!b)' > ref
for i in -R3 -R3f '-R3 -RDS' '-R3f -RDS' '-R3 -RDCS' '-R3f -RDCS'; do
../ltl2tgba -Pref -E -x $i '(X!b R F!a) U (!a | G!b)'
done
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