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

tra_to_tba: finish 05e6e088

* spot/twaalgos/remfin.cc: Actually use propmarks.
* tests/core/det.test, tests/core/remfin.test,
tests/python/automata.ipynb, tests/python/remfin.py,
tests/python/tra2tba.py: Adjust test cases.
parent ff3a3f81
Pipeline #20767 failed with stage
in 319 minutes and 44 seconds
......@@ -273,7 +273,8 @@ namespace spot
state_map[s] = base++;
for (const auto& e: si.inner_edges_of(scc))
{
if (e.acc.has(r) || accedge[aut->edge_number(e)])
unsigned en = aut->edge_number(e);
if ((e.acc | propmarks[en]).has(r) || accedge[en])
continue;
auto src = state_map[e.src];
auto dst = state_map[e.dst];
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de
# Copyright (C) 2013-2020 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -94,16 +94,13 @@ State: 0
State: 1
[!0] 0
[0] 2
[!0] 3
State: 2
[!0] 0
[0] 2
[!0] 3
[0] 4
State: 3 {0}
[!0] 3
State: 4 {0}
[!0] 3
[0] 4
--END--
EOF
......
......@@ -752,7 +752,7 @@ State: 1 {0}
[!0] 0
--END--
HOA: v1
States: 21
States: 19
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
......@@ -768,20 +768,19 @@ State: 1
[0&!1] 6
[0&1] 9
[!0&1] 14
[!0&1] 20
[!0&1] 18
State: 2
[!0&!1] 1
[!0&1] 8
[!0&!1] 20
[!0&!1] 18
State: 3
[0&1] 2
[!0&1] 5
[0&1] 18
State: 4
[0&!1] 4
[0&1] 5
[0&1] 6
[0&!1] 17
[0&!1] 16
State: 5
[0&1] 9
State: 6
......@@ -789,7 +788,6 @@ State: 6
[0&1] 5
[!0&1] 9
[!0&1] 12
[!0&1] 17
State: 7 {0}
[0&!1] 3
[!0&1] 5
......@@ -799,15 +797,12 @@ State: 8
[!0&!1] 3
[!0&1] 4
[!0&1] 8
[!0&1] 12
[!0&1] 13
[!0&1] 17
[!0&!1] 19
State: 9
[!0&1] 2
[0&!1] 6
[0&!1] 11
[!0&1] 18
[!0&1] 17
State: 10 {0}
[0&!1] 11
State: 11 {0}
......@@ -816,25 +811,18 @@ State: 11 {0}
State: 12 {0}
[0&1] 11
State: 13 {0}
[!0&1] 12
[!0&1] 13
State: 14 {0}
[!0&1] 14
State: 15 {0}
[0&1] 16
[!0&1] 17
State: 16 {0}
[!0&1] 18
[0&!1] 16
State: 17 {0}
[0&1] 15
[0&!1] 17
[!0&!1] 18
State: 18 {0}
[!0&!1] 20
State: 19 {0}
[!0&1] 15
[0&1] 18
State: 20 {0}
[0&1] 16
[!0&1] 20
[0&1] 15
[!0&1] 18
--END--
HOA: v1
States: 4
......@@ -1341,7 +1329,7 @@ State: 1 {0}
[0] 1
--END--
HOA: v1
States: 21
States: 19
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
......@@ -1357,20 +1345,19 @@ State: 1
[0&!1] 6
[0&1] 9
[!0&1] 14
[!0&1] 20
[!0&1] 18
State: 2
[!0&!1] 1
[!0&1] 8
[!0&!1] 20
[!0&!1] 18
State: 3
[0&1] 2
[!0&1] 5
[0&1] 18
State: 4
[0&!1] 4
[0&1] 5
[0&1] 6
[0&!1] 17
[0&!1] 16
State: 5
[0&1] 9
State: 6
......@@ -1378,7 +1365,6 @@ State: 6
[0&1] 5
[!0&1] 9
[!0&1] 12
[!0&1] 17
State: 7
[0&!1] 3
[!0&1] 5
......@@ -1388,15 +1374,12 @@ State: 8
[!0&!1] 3
[!0&1] 4
[!0&1] 8
[!0&1] 12
[!0&1] 13
[!0&1] 17
[!0&!1] 19
State: 9
[!0&1] 2
[0&!1] 6
[0&!1] 11
[!0&1] 18
[!0&1] 17
State: 10
[0&!1] 11 {0}
State: 11
......@@ -1405,25 +1388,18 @@ State: 11
State: 12
[0&1] 11 {0}
State: 13
[!0&1] 12
[!0&1] 13 {0}
State: 14
[!0&1] 14 {0}
State: 15
[0&1] 16
[!0&1] 17 {0}
State: 16
[!0&1] 18 {0}
[0&!1] 16 {0}
State: 17
[0&1] 15
[0&!1] 17 {0}
[!0&!1] 18 {0}
State: 18
[!0&!1] 20 {0}
State: 19
[!0&1] 15
[0&1] 18
State: 20
[0&1] 16 {0}
[!0&1] 20 {0}
[0&1] 15 {0}
[!0&1] 18 {0}
--END--
HOA: v1
States: 4
......
This diff is collapsed.
......@@ -92,4 +92,4 @@ State: 2
""")
b = spot.remove_fin(a)
size = (b.num_states(), b.num_edges())
assert size == (5, 17);
assert size == (5, 15);
......@@ -536,7 +536,6 @@ State: 0
State: 1
[!0] 0
[0] 1
[!0] 3
State: 2 {0}
[!0] 2
State: 3 {0}
......
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