Commit 80808133 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

simulation: work on TωA

* src/twaalgos/simulation.cc, src/twaalgos/simulation.hh: Adjust
to work on TωA.  This only require separate acceptance sets.
* src/tests/sim3.test: New test.
* src/tests/Makefile.am: Add it.
parent 0e04b253
......@@ -183,6 +183,7 @@ TESTS_twa = \
maskkeep.test \
simdet.test \
sim2.test \
sim3.test \
ltl2tgba.test \
ltl2neverclaim.test \
ltl2neverclaim-lbtt.test \
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 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
cat >input <<EOF
HOA: v1
States: 7
Start: 0
AP: 2 "b" "a"
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
properties: implicit-labels state-acc complete deterministic
--BODY--
State: 0 {0}
1 5 3 6
State: 1 {1 3}
2 5 4 6
State: 2 {1}
2 5 4 6
State: 3 {0 3}
2 5 4 6
State: 4 {0}
2 5 4 6
State: 5 {1 3}
2 5 4 6
State: 6 {0 3}
2 5 4 6
--END--
EOF
test "`../../bin/autfilt --small input --stats=%S,%s`" = 7,5
......@@ -28,6 +28,7 @@
#include "twaalgos/reachiter.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/sepsets.hh"
#include "misc/bddlt.hh"
// The way we developed this algorithm is the following: We take an
......@@ -160,6 +161,7 @@ namespace spot
// Shortcut used in update_po and go_to_next_it.
typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
int acc_vars;
acc_cond::mark_t all_inf_;
public:
bdd mark_to_bdd(acc_cond::mark_t m)
......@@ -188,9 +190,9 @@ namespace spot
all_class_var_(bddtrue),
original_(in)
{
if (in->acc().uses_fin_acceptance())
if (!has_separate_sets(in))
throw std::runtime_error
("direct_simulation() does not yet support Fin acceptance");
("direct_simulation() requires separate Inf and Fin sets");
// Call get_init_state_number() before anything else as it
// might add a state.
......@@ -201,6 +203,9 @@ namespace spot
assert(ns > 0);
size_a_ = ns;
auto all_inf = in->get_acceptance().used_inf_fin_sets().first;
all_inf_ = all_inf;
// Replace all the acceptance conditions by their complements.
// (In the case of Cosimulation, we also flip the transitions.)
if (Cosimulation)
......@@ -209,7 +214,6 @@ namespace spot
a_->copy_ap_of(in);
a_->copy_acceptance_of(in);
a_->new_states(ns);
auto& acccond = in->acc();
for (unsigned s = 0; s < ns; ++s)
{
......@@ -227,13 +231,13 @@ namespace spot
acc = 0U;
for (auto& td: in->out(t.dst))
{
acc = acccond.comp(td.acc);
acc = td.acc ^ all_inf;
break;
}
}
else
{
acc = acccond.comp(t.acc);
acc = t.acc ^ all_inf;
}
a_->new_transition(t.dst, s, t.cond, acc);
}
......@@ -243,9 +247,8 @@ namespace spot
else
{
a_ = make_twa_graph(in, twa::prop_set::all());
auto& acccond = a_->acc();
for (auto& t: a_->transitions())
t.acc = acccond.comp(t.acc);
t.acc ^= all_inf;
}
assert(a_->num_states() == size_a_);
......@@ -515,6 +518,7 @@ namespace spot
unsigned nb_satoneset = 0;
unsigned nb_minato = 0;
auto all_inf = all_inf_;
// For each class, we will create
// all the transitions between the states.
for (auto& p: bdd_lstate_)
......@@ -580,10 +584,10 @@ namespace spot
bdd cond = bdd_existcomp(cond_acc_dest,
sup_all_atomic_prop);
// Because we have complemented all the acceptance
// conditions on the input automaton, we must
// revert them to create a new transition.
acc = res->acc().comp(acc);
// Because we have complemented all the Inf
// acceptance conditions on the input automaton,
// we must revert them to create a new transition.
acc ^= all_inf;
if (Cosimulation)
{
......
......@@ -33,7 +33,7 @@ namespace spot
/// When the suffixes (letter and acceptance conditions) reachable
/// from one state are included in the suffixes seen by another one,
/// the former state can be merged into the latter. The algorithm is
/// based on the following paper, but generalized to handle TGBA
/// based on the following paper, but generalized to handle TωA
/// directly.
///
/** \verbatim
......@@ -81,7 +81,7 @@ namespace spot
/// state can be merged into the latter.
///
/// Reverse simulation is discussed in the following paper,
/// but generalized to handle TGBA directly.
/// but generalized to handle TωA directly.
/** \verbatim
@InProceedings{ somenzi.00.cav,
author = {Fabio Somenzi and Roderick Bloem},
......
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