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

postproc: simplify the acceptance condition

* spot/twaalgos/postproc.cc: Here.
* spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug
uncovered by the new simplified automata.
* tests/core/satmin2.test, tests/core/sccdot.test,
tests/core/sim3.test, tests/python/decompose.ipynb,
tests/python/satmin.ipynb: Update expected results.
* NEWS: Mention the simplification and the bug.
parent 4532c0c1
......@@ -116,6 +116,10 @@ New in spot 2.5.3.dev (not yet released)
FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4
FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 8 8
- The automaton postprocessor will now simplify acceptance
conditions more aggressively, calling spot::simplify_acceptance()
or spot::cleanup_acceptance() depanding on the optimization level.
- print_dot(), used to print automata in GraphViz's format,
underwent several changes:
......@@ -216,7 +220,10 @@ New in spot 2.5.3.dev (not yet released)
- The HOA parser will now accept Alias: declarations that occur
before AP:.
- the option --allow-dups of randltl now works properly
- The option --allow-dups of randltl now works properly.
- Converting generalized-co-Büchi to Streett using dnf_to_nca()
could produce bogus automata if the input had rejecting SCCs.
Deprecation notice:
......
......@@ -133,7 +133,7 @@ namespace spot
product_states* res_map_; // States of the aug. sub. cons.
scc_info si_; // SCC information.
unsigned nb_states_; // Number of states.
unsigned was_rabin_; // Was it Rabin before Streett?
unsigned was_dnf_; // Was it DNF before Streett?
std::vector<unsigned>* orig_states_; // Match old Rabin st. from new.
std::vector<unsigned>* orig_clauses_; // Associated Rabin clauses.
unsigned orig_num_st_; // Rabin original nb states.
......@@ -148,7 +148,7 @@ namespace spot
bv->set(state);
unsigned clause = 0;
unsigned state = st.first;
if (was_rabin_)
if (was_dnf_)
{
clause = (*orig_clauses_)[state];
assert((int)clause >= 0);
......@@ -194,7 +194,7 @@ namespace spot
const const_twa_graph_ptr ref_power,
std::vector<acc_cond::rs_pair>& pairs,
bool named_states = false,
bool was_rabin = false,
bool was_dnf = false,
unsigned orig_num_st = 0)
: aut_(ref_prod),
state_based_(aut_->prop_state_acc().is_true()),
......@@ -206,10 +206,10 @@ namespace spot
si_(res_, (scc_info_options::TRACK_STATES
| scc_info_options::TRACK_SUCCS)),
nb_states_(res_->num_states()),
was_rabin_(was_rabin),
was_dnf_(was_dnf),
orig_num_st_(orig_num_st ? orig_num_st : ref_prod->num_states())
{
if (was_rabin)
if (was_dnf)
{
orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>>
("original-states");
......
......@@ -39,6 +39,7 @@
#include <spot/twaalgos/parity.hh>
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/rabin2parity.hh>
#include <spot/twaalgos/cleanacc.hh>
namespace spot
{
......@@ -230,6 +231,27 @@ namespace spot
throw std::runtime_error("postprocessor: the Colored setting only works "
"for parity acceptance");
// Attempt to simplify the acceptance condition, unless this is a
// parity automaton and we want parity acceptance in the output.
auto simplify_acc = [&](twa_graph_ptr in)
{
if (PREF_ == Any && level_ == Low)
return in;
if (!(want_parity && in->acc().is_parity()))
{
if (level_ == High)
return simplify_acceptance(in);
else
return cleanup_acceptance(in);
}
if (level_ == High)
return cleanup_parity(in);
return in;
};
a = simplify_acc(a);
if (!a->is_existential() &&
// We will probably have to revisit this condition later.
// Currently, the intent is that postprocessor should never
......@@ -438,6 +460,7 @@ namespace spot
{
dba = tgba_determinize(to_generalized_buchi(sim),
false, det_scc_, det_simul_, det_stutter_);
dba = simplify_acc(dba);
if (level_ != Low)
dba = simulation(dba);
sim = nullptr;
......
......@@ -76,35 +76,32 @@ namespace spot
void
split_dnf_clauses(const acc_cond::acc_code& code)
{
bool one_conjunction = false;
const acc_cond::acc_op root_op = code.back().sub.op;
auto s = code.back().sub.size;
while (s)
auto pos = &code.back();
if (pos->sub.op == acc_cond::acc_op::Or)
--pos;
auto start = &code.front();
while (pos > start)
{
--s;
if (code[s].sub.op == acc_cond::acc_op::And
|| ((one_conjunction = root_op == acc_cond::acc_op::And)))
const unsigned short size = pos[0].sub.size;
if (pos[0].sub.op == acc_cond::acc_op::And)
{
s = one_conjunction ? s + 1 : s;
const unsigned short size = code[s].sub.size;
acc_cond::mark_t fin = {};
acc_cond::mark_t inf = {};
for (unsigned i = 1; i <= size; i += 2)
for (int i = 1; i <= (int)size; i += 2)
{
if (code[s-i].sub.op == acc_cond::acc_op::Fin)
fin |= code[s-i-1].mark;
else if (code[s-i].sub.op == acc_cond::acc_op::Inf)
inf |= code[s-i-1].mark;
if (pos[-i].sub.op == acc_cond::acc_op::Fin)
fin |= pos[-i - 1].mark;
else if (pos[-i].sub.op == acc_cond::acc_op::Inf)
inf |= pos[-i - 1].mark;
else
SPOT_UNREACHABLE();
}
all_clauses_.emplace_back(fin, inf);
set_to_keep_.emplace_back(fin | inf);
s -= size;
}
else if (code[s].sub.op == acc_cond::acc_op::Fin) // Fin
else if (pos[0].sub.op == acc_cond::acc_op::Fin) // Fin
{
auto m1 = code[--s].mark;
auto m1 = pos[-1].mark;
for (unsigned int s : m1.sets())
{
all_clauses_.emplace_back(acc_cond::mark_t({s}),
......@@ -112,9 +109,9 @@ namespace spot
set_to_keep_.emplace_back(acc_cond::mark_t({s}));
}
}
else if (code[s].sub.op == acc_cond::acc_op::Inf) // Inf
else if (pos[0].sub.op == acc_cond::acc_op::Inf) // Inf
{
auto m2 = code[--s].mark;
auto m2 = pos[-1].mark;
all_clauses_.emplace_back(acc_cond::mark_t({}), m2);
set_to_keep_.emplace_back(m2);
}
......@@ -122,6 +119,7 @@ namespace spot
{
SPOT_UNREACHABLE();
}
pos -= size + 1;
}
#if TRACE
trace << "\nPrinting all clauses\n";
......@@ -244,10 +242,12 @@ namespace spot
trace << "accepting clauses\n";
for (unsigned i = 0; i < res.size(); ++i)
{
trace << "scc(" << i << ") --> ";
trace << "scc(" << i << ") -->";
for (auto elt : res[i])
trace << elt << ',';
trace << '\n'
trace << ' ' << elt;
if (si_.is_rejecting_scc(i))
trace << " rej";
trace << '\n';
}
trace << '\n';
#endif
......@@ -341,6 +341,7 @@ namespace spot
{
if (!si_.is_useful_scc(scc))
continue;
trace << "scc #" << scc << '\n';
bool rej_scc = acc_clauses_[scc].empty();
for (auto st : si_.states_of(scc))
......@@ -388,7 +389,7 @@ namespace spot
acc_cond::mark_t m = {};
if (same_scc || state_based_)
m = all_set_to_add_;
m = e.acc | all_set_to_add_;
for (const auto& p_dst : st_repr_[e.dst])
res_->new_edge(src, p_dst.second, e.cond, m);
......
......@@ -335,7 +335,8 @@ HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 2 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))
acc-name: generalized-co-Buchi 2
Acceptance: 2 Fin(0)|Fin(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
......
......@@ -156,7 +156,7 @@ HOA: v1
States: 8
Start: 0
AP: 2 "a" "b"
Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2)
Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -55,25 +55,25 @@ HOA: v1
States: 5
Start: 0
AP: 2 "b" "a"
acc-name: Rabin 2
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
acc-name: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[!1] 1
[1] 3
State: 1 {1 3}
State: 1 {1}
[0&!1] 1
[!0&!1] 2
[0&1] 3
[!0&1] 4
State: 2 {1}
State: 2
[0&!1] 1
[!0&!1] 2
[0&1] 3
[!0&1] 4
State: 3 {0 3}
State: 3 {0 1}
[0&!1] 1
[!0&!1] 2
[0&1] 3
......
This diff is collapsed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
Supports Markdown
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