diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 1b5d452d6..65e022453 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -436,14 +436,20 @@ namespace spot scc_info* given_si) { twa_graph_ptr res; + scc_info* si = given_si; if (aut->prop_inherently_weak()) { + // Create scc_info here, because we will need it to decide + // very-weakness. + if (!si) + si = new scc_info(aut, scc_info_options::TRACK_SUCCS + | scc_info_options::TRACK_STATES_IF_FIN_USED); if (aut->acc().is_t() || aut->acc().is_co_buchi()) res = - scc_filter_apply>>(aut, given_si); + scc_filter_apply>>(aut, si); else res = - scc_filter_apply>>(aut, given_si); + scc_filter_apply>>(aut, si); } else if (aut->acc().is_generalized_buchi()) { @@ -485,6 +491,10 @@ namespace spot { res->prop_weak(true); res->prop_state_acc(true); + if (si->scc_count() == aut->num_states()) + res->prop_very_weak(true); + if (!given_si) + delete si; } return res; } diff --git a/tests/core/dca2.test b/tests/core/dca2.test index eef1d8168..74a24b2e7 100755 --- a/tests/core/dca2.test +++ b/tests/core/dca2.test @@ -67,8 +67,8 @@ while read l_f; do autfilt -q --acceptance-is=Streett-like and.hoa # Streett | Streett autfilt r.hoa --name="($l_f)|!($r_f)" --product-or=l.hoa -S > or.hoa - if ! grep -q ' weak' l.hoa; then - if ! grep -q ' weak' r.hoa; then + if ! grep -q '[ -]weak' l.hoa; then + if ! grep -q '[ -]weak' r.hoa; then autfilt -q -v --acceptance-is=Streett-like or.hoa || exit 1 fi fi diff --git a/tests/core/monitor.test b/tests/core/monitor.test index fc43c6b2c..26f5c5667 100755 --- a/tests/core/monitor.test +++ b/tests/core/monitor.test @@ -98,7 +98,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic stutter-invariant weak +properties: deterministic stutter-invariant very-weak --BODY-- State: 0 {0} [0] 0 diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 40daa2cbc..6d40b7414 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -236,7 +236,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: weak +properties: very-weak --BODY-- State: 0 [t] 0 @@ -270,7 +270,7 @@ AP: 1 "a" acc-name: Rabin 1 Acceptance: 2 Fin(0) & Inf(1) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: weak +properties: very-weak --BODY-- State: 0 [t] 0 @@ -304,7 +304,7 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc stutter-invariant -properties: weak +properties: very-weak --BODY-- State: 0 [t] 0 @@ -338,7 +338,7 @@ AP: 1 "a" acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant weak +properties: stutter-invariant very-weak --BODY-- State: 0 {0} [t] 0 @@ -372,7 +372,7 @@ AP: 1 "a" acc-name: parity min odd 3 Acceptance: 3 Fin(0) & (Inf(1) | Fin(2)) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant weak +properties: stutter-invariant very-weak --BODY-- State: 0 {2} [t] 0 @@ -406,7 +406,7 @@ AP: 1 "a" acc-name: parity max even 3 Acceptance: 3 Inf(2) | (Fin(1) & Inf(0)) properties: trans-labels explicit-labels state-acc colored -properties: stutter-invariant weak +properties: stutter-invariant very-weak --BODY-- State: 0 {1} [t] 0 diff --git a/tests/core/randomize.test b/tests/core/randomize.test index de3059486..259f03d0b 100755 --- a/tests/core/randomize.test +++ b/tests/core/randomize.test @@ -33,7 +33,7 @@ AP: 4 "a" "b" "c" "d" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc stutter-invariant -properties: weak +properties: very-weak --BODY-- State: 0 [0] 1 diff --git a/tests/core/readsave.test b/tests/core/readsave.test index d38e553f2..55c985170 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -779,7 +779,8 @@ Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc deterministic weak +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak --BODY-- State: 0 [1] 2 @@ -810,8 +811,8 @@ AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic -properties: no-univ-branch unambiguous semi-deterministic weak -properties: inherently-weak +properties: no-univ-branch unambiguous semi-deterministic very-weak +properties: weak inherently-weak --BODY-- State: 0 [1] 2 diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 821f9eb61..c3835d294 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -972,7 +972,7 @@ AP: 0 acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic -properties: stutter-invariant weak +properties: stutter-invariant very-weak --BODY-- State: 0 --END-- diff --git a/tests/core/sccsimpl.test b/tests/core/sccsimpl.test index 7211244b5..c62989b13 100755 --- a/tests/core/sccsimpl.test +++ b/tests/core/sccsimpl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2013, 2015 Laboratoire de Recherche et +# Copyright (C) 2011, 2013, 2015, 2018 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -316,7 +316,7 @@ AP: 1 "p0" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic weak +properties: deterministic very-weak --BODY-- State: 0 {0} [t] 0 @@ -331,7 +331,7 @@ AP: 1 "p0" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic weak +properties: deterministic very-weak --BODY-- State: 0 {0} [t] 0 diff --git a/tests/core/wdba2.test b/tests/core/wdba2.test index 82ed64823..fb20d0a25 100755 --- a/tests/core/wdba2.test +++ b/tests/core/wdba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +# Copyright (C) 2012, 2014, 2015, 2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -67,7 +67,7 @@ Start: 2 AP: 1 "p1" acc-name: Buchi Acceptance: 1 Inf(0) -properties: implicit-labels state-acc complete deterministic weak +properties: implicit-labels state-acc complete deterministic very-weak --BODY-- State: 0 {0} 0 0 diff --git a/tests/python/dualize.py b/tests/python/dualize.py index abd3d2ddf..b919eaac0 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -98,7 +98,7 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic stutter-invariant weak +properties: deterministic stutter-invariant very-weak --BODY-- State: 0 {0} [t] 0 diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 5acf3b173..d1bb3793e 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -27,7 +27,8 @@ Start: 0 AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) -properties: trans-labels explicit-labels state-acc deterministic weak +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak --BODY-- State: 0 {0} [0] 1