36d20696bf
This allows fixing issue #388 reported by Victor Khomenko. * spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New method. * tests/python/stutter-inv.ipynb: Use it. * tests/python/stutter.py: New file, with Victor's test case. * tests/Makefile.am: Add python/stutter.py.
279 lines
7.6 KiB
C++
279 lines
7.6 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2013-2019 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/>.
|
|
|
|
#include "config.h"
|
|
#include <spot/twaalgos/word.hh>
|
|
#include <spot/twa/bddprint.hh>
|
|
#include <spot/twa/bdddict.hh>
|
|
#include <spot/tl/parse.hh>
|
|
#include <spot/tl/simplify.hh>
|
|
#include <spot/tl/apcollect.hh>
|
|
|
|
using namespace std::string_literals;
|
|
|
|
namespace spot
|
|
{
|
|
twa_word::twa_word(const twa_run_ptr& run) noexcept
|
|
: dict_(run->aut->get_dict())
|
|
{
|
|
for (auto& i: run->prefix)
|
|
prefix.emplace_back(i.label);
|
|
for (auto& i: run->cycle)
|
|
cycle.emplace_back(i.label);
|
|
dict_->register_all_variables_of(run->aut, this);
|
|
}
|
|
|
|
twa_word::twa_word(const bdd_dict_ptr& dict) noexcept
|
|
: dict_(dict)
|
|
{
|
|
}
|
|
|
|
void
|
|
twa_word::use_all_aps(bdd aps, bool positive)
|
|
{
|
|
bdd def = positive ?
|
|
static_cast<bdd>(bddtrue) : static_cast<bdd>(bddfalse);
|
|
for (bdd& i: prefix)
|
|
i = bdd_satoneset(i, aps, def);
|
|
for (bdd& i: cycle)
|
|
i = bdd_satoneset(i, aps, def);
|
|
}
|
|
|
|
void
|
|
twa_word::simplify()
|
|
{
|
|
// If all the formulas on the cycle are compatible, reduce the
|
|
// cycle to a simple conjunction.
|
|
//
|
|
// For instance
|
|
// !a|!b; b; a&b; cycle{a; b; a&b}
|
|
// can be reduced to
|
|
// !a|!b; b; a&b; cycle{a&b}
|
|
{
|
|
bdd all = bddtrue;
|
|
for (auto& i: cycle)
|
|
all &= i;
|
|
if (all != bddfalse)
|
|
{
|
|
cycle.clear();
|
|
cycle.emplace_back(all);
|
|
}
|
|
}
|
|
// If the last formula of the prefix is compatible with the
|
|
// last formula of the cycle, we can shift the cycle and
|
|
// reduce the prefix.
|
|
//
|
|
// For instance
|
|
// !a|!b; b; a&b; cycle{a&b}
|
|
// can be reduced to
|
|
// !a|!b; cycle{a&b}
|
|
while (!prefix.empty())
|
|
{
|
|
bdd a = prefix.back() & cycle.back();
|
|
if (a == bddfalse)
|
|
break;
|
|
prefix.pop_back();
|
|
cycle.pop_back();
|
|
cycle.push_front(a);
|
|
}
|
|
// Get rid of any disjunction.
|
|
//
|
|
// For instance
|
|
// !a|!b; cycle{a&b}
|
|
// can be reduced to
|
|
// !a&!b; cycle{a&b}
|
|
for (auto& i: prefix)
|
|
i = bdd_satone(i);
|
|
for (auto& i: cycle)
|
|
i = bdd_satone(i);
|
|
}
|
|
|
|
std::ostream&
|
|
operator<<(std::ostream& os, const twa_word& w)
|
|
{
|
|
if (w.cycle.empty())
|
|
throw std::runtime_error("a twa_word may not have an empty cycle");
|
|
auto d = w.get_dict();
|
|
if (!w.prefix.empty())
|
|
for (auto& i: w.prefix)
|
|
{
|
|
bdd_print_formula(os, d, i);
|
|
os << "; ";
|
|
}
|
|
bool notfirst = false;
|
|
os << "cycle{";
|
|
for (auto& i: w.cycle)
|
|
{
|
|
if (notfirst)
|
|
os << "; ";
|
|
notfirst = true;
|
|
bdd_print_formula(os, d, i);
|
|
}
|
|
os << '}';
|
|
return os;
|
|
}
|
|
|
|
namespace
|
|
{
|
|
static void word_parse_error(const std::string& word,
|
|
size_t i, parsed_formula pf)
|
|
{
|
|
std::ostringstream os;
|
|
pf.format_errors(os, word, i);
|
|
throw parse_error(os.str());
|
|
}
|
|
|
|
static void word_parse_error(const std::string& word, size_t i,
|
|
const std::string& message)
|
|
{
|
|
if (i == std::string::npos)
|
|
i = word.size();
|
|
std::ostringstream s;
|
|
s << ">>> " << word << '\n';
|
|
for (auto j = i + 4; j > 0; --j)
|
|
s << ' ';
|
|
s << '^' << '\n';
|
|
s << message << '\n';
|
|
throw parse_error(s.str());
|
|
}
|
|
|
|
static size_t skip_next_formula(const std::string& word, size_t begin)
|
|
{
|
|
bool quoted = false;
|
|
auto size = word.size();
|
|
for (auto j = begin; j < size; ++j)
|
|
{
|
|
auto c = word[j];
|
|
if (!quoted && (c == ';' || c == '}'))
|
|
return j;
|
|
if (c == '"')
|
|
quoted = !quoted;
|
|
else if (quoted && c == '\\')
|
|
++j;
|
|
}
|
|
if (quoted)
|
|
word_parse_error(word, word.size(), "Unclosed string");
|
|
return std::string::npos;
|
|
}
|
|
}
|
|
|
|
twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict)
|
|
{
|
|
atomic_prop_set aps;
|
|
tl_simplifier tls(dict);
|
|
twa_word_ptr tw = make_twa_word(dict);
|
|
size_t i = 0;
|
|
auto ind = i;
|
|
|
|
auto extract_bdd =
|
|
[&](typename twa_word::seq_t& seq)
|
|
{
|
|
auto sub = word.substr(i, ind - i);
|
|
auto pf = spot::parse_infix_boolean(sub);
|
|
if (!pf.errors.empty())
|
|
word_parse_error(word, i, pf);
|
|
atomic_prop_collect(pf.f, &aps);
|
|
seq.emplace_back(tls.as_bdd(pf.f));
|
|
if (word[ind] == '}')
|
|
return true;
|
|
// Skip blanks after semi-colon
|
|
i = word.find_first_not_of(' ', ind + 1);
|
|
return false;
|
|
};
|
|
|
|
// Parse the prefix part. Can be empty.
|
|
while (word.substr(i, 6) != "cycle{"s)
|
|
{
|
|
ind = skip_next_formula(word, i);
|
|
if (ind == std::string::npos)
|
|
word_parse_error(word, word.size(),
|
|
"A twa_word must contain a cycle");
|
|
if (word[ind] == '}')
|
|
word_parse_error(word, ind, "Expected ';' delimiter: "
|
|
"'}' stands for ending a cycle");
|
|
// Exract formula, convert it to bdd and add it to the prefix sequence
|
|
extract_bdd(tw->prefix);
|
|
if (i == std::string::npos)
|
|
word_parse_error(word, ind + 1, "Missing cycle in formula");
|
|
}
|
|
// Consume "cycle{"
|
|
i += 6;
|
|
while (true)
|
|
{
|
|
ind = skip_next_formula(word, i);
|
|
if (ind == std::string::npos)
|
|
word_parse_error(word, word.size(),
|
|
"Missing ';' or '}' after formula");
|
|
// Extract formula, convert it to bdd and add it to the cycle sequence
|
|
// Break if an '}' is encountered
|
|
if (extract_bdd(tw->cycle))
|
|
break;
|
|
if (i == std::string::npos)
|
|
word_parse_error(word, ind + 1,
|
|
"Missing end of cycle character: '}'");
|
|
}
|
|
if (ind != word.size() - 1)
|
|
word_parse_error(word, ind + 1, "Input should be finished after cycle");
|
|
for (auto ap: aps)
|
|
dict->register_proposition(ap, tw.get());
|
|
return tw;
|
|
}
|
|
|
|
twa_graph_ptr twa_word::as_automaton() const
|
|
{
|
|
twa_graph_ptr aut = make_twa_graph(dict_);
|
|
|
|
aut->prop_weak(true);
|
|
aut->prop_universal(true);
|
|
|
|
// Register the atomic propositions used in the word.
|
|
{
|
|
bdd support = bddtrue;
|
|
for (auto b: prefix)
|
|
support &= bdd_support(b);
|
|
for (auto b: cycle)
|
|
support &= bdd_support(b);
|
|
while (support != bddtrue)
|
|
{
|
|
int v = bdd_var(support);
|
|
support = bdd_high(support);
|
|
aut->register_ap(dict_->bdd_map[v].f);
|
|
}
|
|
}
|
|
|
|
size_t i = 0;
|
|
aut->new_states(prefix.size() + cycle.size());
|
|
for (auto b: prefix)
|
|
{
|
|
aut->new_edge(i, i + 1, b);
|
|
++i;
|
|
}
|
|
size_t j = i;
|
|
auto b = cycle.begin();
|
|
auto end = --cycle.end();
|
|
for (; b != end; ++b)
|
|
{
|
|
aut->new_edge(i, i + 1, *b);
|
|
++i;
|
|
}
|
|
// Close the loop
|
|
aut->new_edge(i, j, *b);
|
|
return aut;
|
|
}
|
|
}
|