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

use reduce_parity in translator and posprocessor

* spot/twaalgos/postproc.cc, spot/twaalgos/translate.cc: Here.
* tests/core/genltl.test, tests/core/parity2.test,
tests/core/sccsimpl.test, tests/python/twagraph-internals.ipynb:
Adjust test cases.
* NEWS: Mention it.
parent ebfa3a37
......@@ -114,6 +114,9 @@ New in spot 2.7.5.dev (not yet released)
a better replacement for cleanup_parity() and colorize_parity().
See https://spot.lrde.epita.fr/ipynb/parity.html for examples.
- The postprocessor and translator classes are now using
reduce_parity() for further simplifications.
New in spot 2.7.5 (2019-06-05)
Build:
......
......@@ -198,8 +198,7 @@ namespace spot
tmp = sbacc(tmp);
if (want_parity)
{
if (COLORED_)
colorize_parity_here(tmp);
reduce_parity_here(tmp, COLORED_);
parity_kind kind = parity_kind_any;
parity_style style = parity_style_any;
if ((type_ & ParityMin) == ParityMin)
......@@ -241,16 +240,18 @@ namespace spot
{
if (PREF_ == Any && level_ == Low)
return in;
if (!(want_parity && in->acc().is_parity()))
bool isparity = in->acc().is_parity();
if (isparity && in->is_existential()
&& (type_ == Generic || want_parity))
return reduce_parity(in);
if (!(want_parity && isparity))
{
if (level_ == High)
return simplify_acceptance(in);
else
return cleanup_acceptance(in);
}
if (level_ == High)
return cleanup_parity(in);
return in;
return cleanup_parity(in);
};
a = simplify_acc(a);
......
......@@ -28,6 +28,7 @@
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/hoa.hh>
namespace spot
{
......@@ -230,7 +231,9 @@ namespace spot
om = *opt_;
om.set("ltl-split", 0);
translator translate_without_split(simpl_, &om);
translate_without_split.set_pref(pref_);
// Never force colored automata at intermediate steps.
// This is best added at the very end.
translate_without_split.set_pref(pref_ & ~Colored);
translate_without_split.set_level(level_);
translate_without_split.set_type(type_);
auto transrun = [&](formula f)
......@@ -302,6 +305,11 @@ namespace spot
aut = product_susp(aut, susp_aut);
else
aut = product_or_susp(aut, susp_aut);
//if (aut && susp_aut)
// {
// print_hoa(std::cerr << "AUT\n", aut) << '\n';
// print_hoa(std::cerr << "SUSPAUT\n", susp_aut) << '\n';
// }
}
if (leading_x > 0)
{
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
# Copyright (C) 2016-2019 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -185,28 +185,28 @@ cat >exp<<EOF
"ms-example=4,3",11,11
"ms-example=4,4",12,12
"ms-phi-r=0",1,2
"ms-phi-r=1",1,16
"ms-phi-r=2",1,29
"ms-phi-s=0",1,5
"ms-phi-s=1",1,8
"ms-phi-s=2",1,494
"ms-phi-r=1",1,12
"ms-phi-r=2",1,28
"ms-phi-s=0",1,3
"ms-phi-s=1",1,7
"ms-phi-s=2",1,375
"ms-phi-h=0",1,1
"ms-phi-h=1",2,3
"ms-phi-h=2",4,7
"ms-phi-h=3",8,15
"ms-phi-h=4",16,31
"gf-equiv=0",1,1
"gf-equiv=1",1,4
"gf-equiv=2",1,8
"gf-equiv=3",1,21
"gf-equiv=4",1,81
"gf-equiv=5",1,431
"gf-equiv=1",1,3
"gf-equiv=2",1,7
"gf-equiv=3",1,20
"gf-equiv=4",1,80
"gf-equiv=5",1,430
"gf-implies=0",1,1
"gf-implies=1",1,5
"gf-implies=2",1,12
"gf-implies=3",1,41
"gf-implies=4",1,186
"gf-implies=5",1,1047
"gf-implies=1",1,4
"gf-implies=2",1,11
"gf-implies=3",1,33
"gf-implies=4",1,131
"gf-implies=5",1,653
"gf-equiv-xn=1",2,2
"gf-equiv-xn=2",4,4
"gf-equiv-xn=3",8,8
......
......@@ -317,14 +317,14 @@ State: 1
[1&2] 4 {2}
State: 2
[!0] 1 {2}
[0&1&2] 2 {1}
[0&!1&2] 2 {2}
[0&1&2] 2 {1}
State: 3
[0] 3 {2}
[0&1&2] 4 {2}
State: 4
[0&1&2] 4 {1}
[0&!1&2] 4 {2}
[0&1&2] 4 {1}
--END--
HOA: v1
name: "FGa"
......@@ -804,7 +804,7 @@ properties: trans-labels explicit-labels trans-acc deterministic
State: 0
[0&!1 | 0&!2] 0
[!0] 1
[0&1&2] 2 {1}
[0&1&2] 2
State: 1
[!1 | !2] 3
[1&2] 4
......@@ -815,7 +815,7 @@ State: 2
[0&1&2] 2 {1}
State: 3
[0&!1 | 0&!2] 3
[0&1&2] 4 {1}
[0&1&2] 4
State: 4
[0&!2] 3 {0}
[0&!1&2] 4
......@@ -865,7 +865,7 @@ properties: trans-labels explicit-labels trans-acc deterministic
State: 0
[0&!1 | 0&!2] 0
[!0] 1
[0&1&2] 2 {1}
[0&1&2] 2
State: 1
[!1 | !2] 3
[1&2] 4
......@@ -876,7 +876,7 @@ State: 2
[0&1&2] 2 {1}
State: 3
[0&!1 | 0&!2] 3
[0&1&2] 4 {1}
[0&1&2] 4
State: 4
[0&!2] 3 {0}
[0&!1&2] 4
......@@ -926,7 +926,7 @@ properties: trans-labels explicit-labels trans-acc deterministic
State: 0
[0&!1 | 0&!2] 0
[!0] 1
[0&1&2] 2 {0}
[0&1&2] 2
State: 1
[!1 | !2] 3
[1&2] 4
......@@ -937,7 +937,7 @@ State: 2
[0&1&2] 2 {0}
State: 3
[0&!1 | 0&!2] 3
[0&1&2] 4 {0}
[0&1&2] 4
State: 4
[0&!2] 3 {1}
[0&!1&2] 4
......@@ -988,22 +988,22 @@ properties: deterministic
State: 0
[0&!1 | 0&!2] 0 {2}
[!0] 1 {2}
[0&1&2] 2 {1}
[0&1&2] 2 {2}
State: 1
[!1 | !2] 3 {2}
[1&2] 4 {2}
State: 2
[0&!2] 0 {0}
[!0] 1 {2}
[0&1&2] 2 {1}
[0&!1&2] 2 {2}
[0&1&2] 2 {1}
State: 3
[0&!1 | 0&!2] 3 {2}
[0&1&2] 4 {1}
[0&1&2] 4 {2}
State: 4
[0&!2] 3 {0}
[0&1&2] 4 {1}
[0&!1&2] 4 {2}
[0&1&2] 4 {1}
--END--
HOA: v1
name: "FGa"
......@@ -1050,22 +1050,22 @@ properties: deterministic
State: 0
[0&!1 | 0&!2] 0 {2}
[!0] 1 {2}
[0&1&2] 2 {1}
[0&1&2] 2 {2}
State: 1
[!1 | !2] 3 {2}
[1&2] 4 {2}
State: 2
[0&!2] 0 {0}
[!0] 1 {2}
[0&1&2] 2 {1}
[0&!1&2] 2 {2}
[0&1&2] 2 {1}
State: 3
[0&!1 | 0&!2] 3 {2}
[0&1&2] 4 {1}
[0&1&2] 4 {2}
State: 4
[0&!2] 3 {0}
[0&1&2] 4 {1}
[0&!1&2] 4 {2}
[0&1&2] 4 {1}
--END--
HOA: v1
name: "FGa"
......@@ -1112,7 +1112,7 @@ properties: deterministic
State: 0
[0&!1 | 0&!2] 0 {1}
[!0] 1 {1}
[0&1&2] 2 {2}
[0&1&2] 2 {1}
State: 1
[!1 | !2] 3 {1}
[1&2] 4 {1}
......@@ -1123,7 +1123,7 @@ State: 2
[0&1&2] 2 {2}
State: 3
[0&!1 | 0&!2] 3 {1}
[0&1&2] 4 {2}
[0&1&2] 4 {1}
State: 4
[0&!2] 3 {3}
[0&!1&2] 4 {1}
......@@ -1135,20 +1135,17 @@ diff expected3 res3
cat >expected4<<EOF
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 1 {1}
State: 1
[0] 0
[!0] 0 {0}
[0] 1 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1199,20 +1196,17 @@ State: 4
--END--
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 1 {1}
State: 1
[0] 0
[!0] 0 {0}
[0] 1 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1263,20 +1257,17 @@ State: 4
--END--
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: parity max even 2
Acceptance: 2 Fin(1) & Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 1 {0}
State: 1
[0] 0 {0}
[!0] 0 {1}
[0] 1 {0}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1327,20 +1318,17 @@ State: 4
--END--
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
acc-name: parity max even 2
Acceptance: 2 Fin(1) & Inf(0)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0 {2}
[0] 1 {1}
State: 1
[!0] 0 {0}
[0] 1 {1}
[0] 0 {0}
[!0] 0 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1392,20 +1380,17 @@ State: 4
--END--
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0] 0 {2}
[0] 1 {1}
State: 1
[0] 0 {1}
[!0] 0 {0}
[0] 1 {1}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1457,20 +1442,17 @@ State: 4
--END--
HOA: v1
name: "FGa"
States: 2
States: 1
Start: 0
AP: 1 "a"
acc-name: parity max even 4
Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))
acc-name: parity max even 2
Acceptance: 2 Fin(1) & Inf(0)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 0 {0}
[!0] 0 {1}
[0] 1 {2}
State: 1
[!0] 0 {3}
[0] 1 {2}
--END--
HOA: v1
name: "G(Fa & Fb)"
......@@ -1535,7 +1517,7 @@ cat >expected <<EOF
"input.states","output.states"
2,3
3,15
4,129
5,2057
4,120
5,1801
EOF
diff sizes.csv expected
......@@ -292,16 +292,16 @@ HOA: v1
States: 2
Start: 1
AP: 1 "p0"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[t] 0 {1}
State: 0 {0}
[t] 0
State: 1
[0] 0
[!0] 1 {0}
[!0] 1
--END--
EOF
cat output
......
This diff is collapsed.
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