alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Slight improvement of the determinization

Browse source 
* spot/twaalgos/determinize.cc: the acceptance condition
  of the determinized automaton should be simpler
* tests/core/safra.test, tests/python/simstate.py: update tests
This commit is contained in:
Maximilien Colange 2018-02-08 18:15:34 +01:00
parent e945beb607
commit 41d5e44914
3 changed files with 42 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/twaalgos/determinize.cc
View file

@ -26,7 +26,6 @@
#include <set> #include <set>
#include <map> #include <map>
#include <spot/misc/bddlt.hh> #include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/determinize.hh> #include <spot/twaalgos/determinize.hh>
@ -34,7 +33,7 @@
#include <spot/twaalgos/sccfilter.hh> #include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/simulation.hh> #include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/parity.hh>
namespace spot namespace spot
{ {
@ -448,15 +447,6 @@ namespace spot
return res; return res;
} }
// Used to remove all acceptance whose value is above or equal to max_acc
void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
{
assert(max_acc < 32);
unsigned mask = (1 << max_acc) - 1;
for (auto& t: aut->edges())
t.acc &= mask;
}
struct compare struct compare
{ {
bool bool
@ -961,20 +951,23 @@ namespace spot
if (s.color_ != -1U) if (s.color_ != -1U)
{ {
res->new_edge(src_num, dst_num, s.cond(), {s.color_}); res->new_edge(src_num, dst_num, s.cond(), {s.color_});
// We only care about green acc which are odd
if (s.color_ % 2 == 1)
sets = std::max(s.color_ + 1, sets); sets = std::max(s.color_ + 1, sets);
} }
else else
res->new_edge(src_num, dst_num, s.cond()); res->new_edge(src_num, dst_num, s.cond());
} }
} }
remove_dead_acc(res, sets); // Green and red colors work in pairs, so the number of parity conditions is
// necessarily even.
if (sets % 2 == 1)
sets += 1;
// Acceptance is now min(odd) since we can emit Red on paths 0 with new opti // Acceptance is now min(odd) since we can emit Red on paths 0 with new opti
res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets)); res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
res->prop_universal(true); res->prop_universal(true);
res->prop_state_acc(false); res->prop_state_acc(false);
cleanup_parity_here(res);
if (pretty_print) if (pretty_print)
res->set_named_prop("state-names", print_debug(aut, seen)); res->set_named_prop("state-names", print_debug(aut, seen));
return res; return res;

22
tests/core/safra.test
View file

@ -45,15 +45,15 @@ HOA: v1
States: 4 States: 4
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: Rabin 1 acc-name: Buchi
Acceptance: 2 Fin(0) & Inf(1) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic properties: trans-labels explicit-labels trans-acc deterministic
--BODY-- --BODY--
State: 0 State: 0
[0] 1 [0] 1
State: 1 State: 1
[!0&1] 2 [!0&1] 2
[0] 3 {1} [0] 3 {0}
State: 2 State: 2
[0&!1] 0 [0&!1] 0
[!0&1] 2 [!0&1] 2
@ -90,27 +90,27 @@ HOA: v1
States: 5 States: 5
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: Rabin 1 acc-name: Buchi
Acceptance: 2 Fin(0) & Inf(1) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic properties: trans-labels explicit-labels trans-acc deterministic
--BODY-- --BODY--
State: 0 State: 0
[0] 1 [0] 1
State: 1 State: 1
[0&!1] 1 [0&!1] 1
[!0&1] 2 {1} [!0&1] 2 {0}
[0&1] 3 [0&1] 3
State: 2 State: 2
[0&!1] 0 [0&!1] 0
[!0&1] 2 {1} [!0&1] 2 {0}
[0&1] 3 [0&1] 3
State: 3 State: 3
[0&1] 1 {1} [0&1] 1 {0}
[!0&1] 2 {1} [!0&1] 2 {0}
[0&!1] 4 [0&!1] 4
State: 4 State: 4
[0] 1 {1} [0] 1 {0}
[!0&1] 2 {1} [!0&1] 2 {0}
--END-- --END--
EOF EOF

46
tests/python/simstate.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement
# de l'Epita # de l'Epita
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -70,26 +70,26 @@ assert daut.to_str() == """HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 2 "p1" "p0" AP: 2 "p1" "p0"
acc-name: parity min odd 4 acc-name: parity min even 3
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) Acceptance: 3 Inf(0) | (Fin(1) & Inf(2))
properties: trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant properties: deterministic stutter-invariant
--BODY-- --BODY--
State: 0 "{₀[0]₀}" State: 0 "{₀[0]₀}"
[!0&!1] 0 [!0&!1] 0
[!0&1] 0 [!0&1] 0
[0&!1] 0 {1} [0&!1] 0 {0}
[0&1] 1 {3} [0&1] 1 {2}
State: 1 "{₀[0]{₂[2]₂}₀}{₁[1]₁}" State: 1 "{₀[0]{₂[2]₂}₀}{₁[1]₁}"
[!0&!1] 0 {2} [!0&!1] 0 {1}
[!0&1] 2 [!0&1] 2
[0&!1] 0 {1} [0&!1] 0 {0}
[0&1] 1 {3} [0&1] 1 {2}
State: 2 "{₀[0]₀}{₁[1]₁}" State: 2 "{₀[0]₀}{₁[1]₁}"
[!0&!1] 0 {2} [!0&!1] 0 {1}
[!0&1] 2 [!0&1] 2
[0&!1] 0 {1} [0&!1] 0 {0}
[0&1] 1 {3} [0&1] 1 {2}
--END--""" --END--"""
aut = spot.automaton(""" aut = spot.automaton("""
@ -113,8 +113,8 @@ assert daut.to_str() == """HOA: v1
States: 12 States: 12
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: parity min odd 4 acc-name: Buchi
Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic properties: trans-labels explicit-labels trans-acc deterministic
--BODY-- --BODY--
State: 0 "{₀[0#0,0#1]₀}" State: 0 "{₀[0#0,0#1]₀}"
@ -123,7 +123,7 @@ State: 0 "{₀[0#0,0#1]₀}"
[0&1] 2 [0&1] 2
State: 1 "{₀[1#1]₀}" State: 1 "{₀[1#1]₀}"
[!0&1] 0 [!0&1] 0
[0&!1] 3 {1} [0&!1] 3 {0}
[0&1] 4 [0&1] 4
State: 2 "{₀[0#0,0#1] [1#1]₀}" State: 2 "{₀[0#0,0#1] [1#1]₀}"
[!0&1] 2 [!0&1] 2
@ -147,24 +147,24 @@ State: 6 "{₀[0#0,0#1] [1#0]₀}"
[0&1] 9 [0&1] 9
State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}" State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}"
[!0&1] 10 [!0&1] 10
[0&!1] 6 {1} [0&!1] 6 {0}
[0&1] 9 {1} [0&1] 9 {0}
State: 8 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}" State: 8 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}"
[!0&1] 2 {1} [!0&1] 2 {0}
[0&!1] 6 {1} [0&!1] 6 {0}
[0&1] 9 {1} [0&1] 9 {0}
State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}" State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}"
[!0&1] 2 [!0&1] 2
[0&!1] 4 [0&!1] 4
[0&1] 5 [0&1] 5
State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}" State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}"
[!0&1] 7 [!0&1] 7
[0&!1] 4 {3} [0&!1] 4 {0}
[0&1] 11 [0&1] 11
State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
[!0&1] 2 {1} [!0&1] 2 {0}
[0&!1] 6 {1} [0&!1] 6 {0}
[0&1] 9 {1} [0&1] 9 {0}
--END--""" --END--"""
a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)') a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')