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

decompose_strength: work with inherently weak SCCs

Browse source 
* wrap/python/tests/decompose.ipynb: Adjust text.
* spot/twaalgos/strength.hh, spot/twaalgos/strength.cc:
Adjust to extract inherently weak SCCs instead of weak SCCs.  This gets
rids of the special handling for the "corner cases".
* spot/tests/strength.test: Adjust.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-09 15:50:13 +01:00
parent 9bbcf85b3a
commit 2e15ed959d
5 changed files with 102 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -29,6 +29,10 @@ New in spot 1.99.6a (not yet released)
check_strength() has been modified to also check inherently weak check_strength() has been modified to also check inherently weak
automata. automata.
* decompose_strength() is now extracting inherently weak SCCs
instead of just weak SCCs. This gets rid of some corner cases
that used to require ad hoc handling.
Python: Python:
Documentation: Documentation:

60
spot/tests/strength.test
View file

@ -264,6 +264,21 @@ State: 1 {0}
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 0 AP: 0
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
@ -334,20 +349,6 @@ State: 2
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1
States: 2
Start: 0
AP: 2 "a" "c" AP: 2 "a" "c"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
@ -393,6 +394,21 @@ State: 1 {0}
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic weak
--BODY--
State: 0 {0}
[0] 1
[!0] 0
State: 1 {0}
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 0 AP: 0
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
@ -444,20 +460,6 @@ State: 4
--END-- --END--
/******************************/ /******************************/
HOA: v1 HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[0] 1 {1}
[!0] 0 {0}
State: 1
[t] 0 {0}
--END--
HOA: v1
States: 1 States: 1
Start: 0 Start: 0
AP: 1 "a" AP: 1 "a"
@ -523,7 +525,7 @@ Start: 0
AP: 1 "a" AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1) Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic properties: deterministic weak
--BODY-- --BODY--
State: 0 State: 0
[0] 1 {1} [0] 1 {1}

2
spot/twaalgos/strength.cc
View file

@ -199,7 +199,7 @@ namespace spot
{ {
if (si.is_accepting_scc(i)) if (si.is_accepting_scc(i))
{ {
if (all_accepting | is_weak_scc(si, i)) if (all_accepting | is_inherently_weak_scc(si, i))
{ {
if (keep & Weak) if (keep & Weak)
{ {

14
spot/twaalgos/strength.hh
View file

@ -87,15 +87,21 @@ namespace spot
/// ///
/// The string \a keep should be a non-empty combination of /// The string \a keep should be a non-empty combination of
/// the following letters: /// the following letters:
/// - 'w': keep only weak SCCs (i.e., SCCs in which all transitions belong /// - 'w': keep only inherently weak SCCs (i.e., SCCs in which
/// to the same acceptance sets) that are not terminal. /// all transitions belong to the same acceptance sets) that
/// - 't': keep terminal SCCs (i.e., weak SCCs that are complete) /// are not terminal.
/// - 's': keep strong SCCs (i.e., SCCs that are not weak). /// - 't': keep terminal SCCs (i.e., inherently weak SCCs that are complete)
/// - 's': keep strong SCCs (i.e., SCCs that are not inherently weak).
/// ///
/// This algorithm returns a subautomaton that contains all SCCs of the /// This algorithm returns a subautomaton that contains all SCCs of the
/// requested strength, plus any upstream SCC (but adjusted not to be /// requested strength, plus any upstream SCC (but adjusted not to be
/// accepting). /// accepting).
/// ///
/// The definition are basically those used in the following paper,
/// except that we extra the "inherently weak" part instead of the
/// weak part because we can now test for inherent weakness
/// efficiently enough (not enumerating all cycles as suggested in
/// the paper).
/** \verbatim /** \verbatim
@inproceedings{renault.13.tacas, @inproceedings{renault.13.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice

115
wrap/python/tests/decompose.ipynb
View file

@ -18,7 +18,7 @@
"version": "3.4.3+" "version": "3.4.3+"
}, },
"name": "", "name": "",
"signature": "sha256:b3b36fe78a04d878ed9e49766fcef5febec464e5c25ad302dd1f446e45b2fd36" "signature": "sha256:ddf44352825d3260c20b0a4d29b4972c9cd5be57b3a48bcdf8afe8acaee5eba6"
}, },
"nbformat": 3, "nbformat": 3,
"nbformat_minor": 0, "nbformat_minor": 0,
@ -48,14 +48,16 @@
"\n", "\n",
"# Basics\n", "# Basics\n",
"\n", "\n",
"Let's define the following strengths of SCCs:\n", "Let's define the following strengths of accepting SCCs:\n",
"\n", "\n",
"- an accepting SCC is **weak** if all its transitions belong to the same acceptance sets\n", "- an accepting SCC is **inherently weak** if it does not contain any rejecting cycle\n",
"- an accepting SCC is **terminal** if it is *weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)\n", "- an accepting SCC is **inherently terminal** if it is *inherently weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)\n",
"- an accepting SCC is **strictly weak** if it is *weak* and not complete (in other words: *weak* but not *terminal*)\n", "- an accepting SCC is **strictly inherently weak** if it is *inherently weak* and not complete (in other words: *weak* but not *terminal*)\n",
"- an accepting SCC is **strong** if it is not weak.\n", "- an accepting SCC is **strong** if it is not inherently weak.\n",
"\n", "\n",
"The strengths **strong**, **stricly weak**, and **terminal** define a partition of all accepting SCCs. The following B\u00fcchi automaton has 4 SCCs, and its 3 accepting SCCs show an example of each strength." "The strengths **strong**, **stricly inherently weak**, and **inherently terminal** define a partition of all accepting SCCs. The following B\u00fcchi automaton has 4 SCCs, and its 3 accepting SCCs show an example of each strength.\n",
"\n",
"Note: the reason we use the word *inherently* is that the *weak* and *terminal* properties are usually defined syntactically: an accepting SCC would be weak if all its transitions belong to the same acceptance sets. This syntactic criterion is a sufficient condition for an accepting SCC to not have any rejecting cycle, but it is not necessary. Hence a *weak* SCC is *inherently weak*; but while an *inherently weak* SCC is not necessarily *weak*, it can be modified to be *weak* without alterning the langage."
] ]
}, },
{ {
@ -210,7 +212,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0f7a50> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048a20> >"
] ]
} }
], ],
@ -224,11 +226,11 @@
"\n", "\n",
"The letters used for this specification are as follows:\n", "The letters used for this specification are as follows:\n",
"\n", "\n",
"- `t`: terminal\n", "- `t`: (inherently) terminal\n",
"- `w`: strictly weak\n", "- `w`: (strictly inherently) weak\n",
"- `s`: strong\n", "- `s`: strong\n",
"\n", "\n",
"For instance if we want to preserve only the **strictly weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it. However the SCC above is not stricly weak, so it should not accept any word in the new automaton." "For instance if we want to preserve only the **strictly inherently weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it. However the SCC above is not stricly weak, so it should not accept any word in the new automaton."
] ]
}, },
{ {
@ -327,7 +329,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0f79c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048990> >"
] ]
} }
], ],
@ -337,7 +339,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"Similarly, we can extract all the behaviors captured by the **terminal** part of the automaton:" "Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:"
] ]
}, },
{ {
@ -468,7 +470,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0f7990> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f73400489c0> >"
] ]
} }
], ],
@ -478,7 +480,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"Here is the strong part:" "Here is the **strong** part:"
] ]
}, },
{ {
@ -558,7 +560,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0f7a20> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7340048bd0> >"
] ]
} }
], ],
@ -635,7 +637,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a3f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f3c0> >"
] ]
} }
], ],
@ -751,7 +753,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a0f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f060> >"
] ]
}, },
{ {
@ -875,7 +877,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a420> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f3f0> >"
] ]
}, },
{ {
@ -1018,7 +1020,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a0f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f060> >"
] ]
} }
], ],
@ -1030,7 +1032,7 @@
"source": [ "source": [
"# Generalized acceptance\n", "# Generalized acceptance\n",
"\n", "\n",
"There is (almost, see below) nothing that prevents the above decomposition to work with other types of acceptance.\n", "There is nothing that prevents the above decomposition to work with other types of acceptance.\n",
"\n", "\n",
"## Rabin\n", "## Rabin\n",
"\n", "\n",
@ -1423,7 +1425,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcf801c60> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f090> >"
] ]
} }
], ],
@ -1748,7 +1750,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a0c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f0c0> >"
] ]
}, },
{ {
@ -1945,7 +1947,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a0f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f060> >"
] ]
}, },
{ {
@ -2125,7 +2127,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a0c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f0c0> >"
] ]
} }
], ],
@ -2137,7 +2139,7 @@
"source": [ "source": [
"Note how the two weak automata (i.e., stricly weak and terminal) are now using a B\u00fcchi acceptance condition (because that is sufficient for weak automata) while the strong automaton inherited the original acceptance condition.\n", "Note how the two weak automata (i.e., stricly weak and terminal) are now using a B\u00fcchi acceptance condition (because that is sufficient for weak automata) while the strong automaton inherited the original acceptance condition.\n",
"\n", "\n",
"When extracting multiple strengths and one of the strength is **strong**, we preserve the original acceptance. For instance extracting **strong** and **terminal** gives the following automaton, where only **stricly weak** SCCs have become rejecting." "When extracting multiple strengths and one of the strength is **strong**, we preserve the original acceptance. For instance extracting **strong** and **inherently terminal** gives the following automaton, where only **stricly inherently weak** SCCs have become rejecting."
] ]
}, },
{ {
@ -2460,7 +2462,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11ac00> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006fbd0> >"
] ]
} }
], ],
@ -2477,7 +2479,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n", "for (name, opt) in (('inherently terminal', 't'), ('strictly inherently weak', 'w'), ('strong', 's')):\n",
" a = spot.decompose_strength(aut, opt).postprocess('deterministic', 'SBAcc')\n", " a = spot.decompose_strength(aut, opt).postprocess('deterministic', 'SBAcc')\n",
" a.set_name(name)\n", " a.set_name(name)\n",
" display(a)" " display(a)"
@ -2500,7 +2502,7 @@
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 167)\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 167)\">\n",
"<title>G</title>\n", "<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-167 410.74,-167 410.74,4 -4,4\"/>\n", "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-167 410.74,-167 410.74,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"177.37\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">terminal</text>\n", "<text text-anchor=\"start\" x=\"142.87\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">inherently terminal</text>\n",
"<text text-anchor=\"start\" x=\"182.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n", "<text text-anchor=\"start\" x=\"182.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"204.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n", "<text text-anchor=\"start\" x=\"204.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"220.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n", "<text text-anchor=\"start\" x=\"220.37\" y=\"-134.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
@ -2604,7 +2606,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11af90> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006ff60> >"
] ]
}, },
{ {
@ -2622,7 +2624,7 @@
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 354)\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 354)\">\n",
"<title>G</title>\n", "<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-354 413.74,-354 413.74,4 -4,4\"/>\n", "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-354 413.74,-354 413.74,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"164.87\" y=\"-335.8\" font-family=\"Lato\" font-size=\"14.00\">strictly weak</text>\n", "<text text-anchor=\"start\" x=\"130.87\" y=\"-335.8\" font-family=\"Lato\" font-size=\"14.00\">strictly inherently weak</text>\n",
"<text text-anchor=\"start\" x=\"183.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n", "<text text-anchor=\"start\" x=\"183.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"205.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n", "<text text-anchor=\"start\" x=\"205.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"221.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n", "<text text-anchor=\"start\" x=\"221.87\" y=\"-321.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
@ -2723,7 +2725,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11acf0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006fcc0> >"
] ]
}, },
{ {
@ -2903,7 +2905,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a450> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f6c0> >"
] ]
} }
], ],
@ -3260,7 +3262,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c2120> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d0f0> >"
] ]
} }
], ],
@ -3270,7 +3272,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n", "for (name, opt) in (('inherently terminal', 't'), ('strictly inherently weak', 'w'), ('strong', 's')):\n",
" a = spot.decompose_strength(aut, opt)\n", " a = spot.decompose_strength(aut, opt)\n",
" a.set_name(name)\n", " a.set_name(name)\n",
" display(a)" " display(a)"
@ -3293,7 +3295,7 @@
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.688337 0.688337) rotate(0) translate(4 519)\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.688337 0.688337) rotate(0) translate(4 519)\">\n",
"<title>G</title>\n", "<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-519 978.96,-519 978.96,4 -4,4\"/>\n", "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-519 978.96,-519 978.96,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"461.48\" y=\"-500.8\" font-family=\"Lato\" font-size=\"14.00\">terminal</text>\n", "<text text-anchor=\"start\" x=\"426.98\" y=\"-500.8\" font-family=\"Lato\" font-size=\"14.00\">inherently terminal</text>\n",
"<text text-anchor=\"start\" x=\"466.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n", "<text text-anchor=\"start\" x=\"466.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"488.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n", "<text text-anchor=\"start\" x=\"488.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"504.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n", "<text text-anchor=\"start\" x=\"504.48\" y=\"-486.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
@ -3550,7 +3552,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c20c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d090> >"
] ]
}, },
{ {
@ -3568,7 +3570,7 @@
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.909091 0.909091) rotate(0) translate(4 392)\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.909091 0.909091) rotate(0) translate(4 392)\">\n",
"<title>G</title>\n", "<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-392 587.22,-392 587.22,4 -4,4\"/>\n", "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-392 587.22,-392 587.22,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"251.61\" y=\"-373.8\" font-family=\"Lato\" font-size=\"14.00\">strictly weak</text>\n", "<text text-anchor=\"start\" x=\"217.61\" y=\"-373.8\" font-family=\"Lato\" font-size=\"14.00\">strictly inherently weak</text>\n",
"<text text-anchor=\"start\" x=\"270.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n", "<text text-anchor=\"start\" x=\"270.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"292.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n", "<text text-anchor=\"start\" x=\"292.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"308.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n", "<text text-anchor=\"start\" x=\"308.61\" y=\"-359.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
@ -3702,7 +3704,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a450> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f6c0> >"
] ]
}, },
{ {
@ -3839,7 +3841,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c20c0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d090> >"
] ]
} }
], ],
@ -3851,7 +3853,7 @@
"source": [ "source": [
"The subtlety of Streett acceptance is that if a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.\n", "The subtlety of Streett acceptance is that if a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.\n",
"\n", "\n",
"This is easy to understand using an example. In the following extraction of the **strong** and **terminal** parts, the rejecting SCCs (that were either rejecting or strictly weak originally) have been labeled by the same acceptance sets, to ensure that they are rejected." "This is easy to understand using an example. In the following extraction of the **strong** and **inherently terminal** parts, the rejecting SCCs (that were either rejecting or strictly inherently weak originally) have been labeled by the same acceptance sets, to ensure that they are rejected."
] ]
}, },
{ {
@ -4142,7 +4144,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c2210> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d1e0> >"
] ]
} }
], ],
@ -4154,15 +4156,13 @@
"source": [ "source": [
"## Corner cases\n", "## Corner cases\n",
"\n", "\n",
"Here is the reason we said there is almost nothing preventing the decomposition to work for any acceptance condition.\n", "When the acceptance condition is always satisfiable, all non-trivial SCCs are accepting, and inherently weak.\n",
"To disable SCCs like above, the `decompose_strength()` must be able to find a set of acceptance sets to put those SCCs\n",
"in such that they will be rejected. This is impossible if the acceptance condition is always satisifiable.\n",
"\n", "\n",
"This include acceptances like `Acceptance: 0 t`, but also trickier ones like `Acceptance: 1 Inf(0) | Fin(0)` that you can make as complex as you fancy.\n", "This include acceptances like `Acceptance: 0 t`, but also trickier ones like `Acceptance: 1 Inf(0) | Fin(0)` that you can make as complex as you fancy.\n",
"\n", "\n",
"### `Acceptance: 0 t`\n", "### `Acceptance: 0 t`\n",
"\n", "\n",
"This is the least problematic case. Because automata with this acceptance are necessary weak, there is reason to extract the **strong** strength, and extracting the other two strengths will work as expected:" "This occur frequently whant translating LTL formulas that are safety properties:"
] ]
}, },
{ {
@ -4255,7 +4255,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c2390> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d360> >"
] ]
} }
], ],
@ -4347,7 +4347,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c23f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d3c0> >"
] ]
}, },
{ {
@ -4413,7 +4413,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c23f0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d3c0> >"
] ]
} }
], ],
@ -4499,7 +4499,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c2450> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d420> >"
] ]
} }
], ],
@ -4518,7 +4518,7 @@
"source": [ "source": [
"### `Acceptance: 1 Inf(0) | Fin(0)`\n", "### `Acceptance: 1 Inf(0) | Fin(0)`\n",
"\n", "\n",
"This acceptance could be replaced by `Acceptance: 0 t` without altering the language of the automaton. However its use of acceptance sets allows us to define some automata with strong SCCs." "This acceptance could be replaced by `Acceptance: 0 t` without altering the language of the automaton. However its use of acceptance sets allows us to define some automata with SCCs that are *inherently weak* but not *weak*."
] ]
}, },
{ {
@ -4654,7 +4654,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c24e0> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f733338d4b0> >"
] ]
} }
], ],
@ -4664,10 +4664,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"By our definitions, SCC $\\{0\\}$ is stricly weak, SCC $\\{1,2\\}$ is strong, and SCC $\\{3\\}$ is terminal.\n", "By our definitions, SCC $\\{0\\}$ and $\\{1,2\\}$ are inherently weak, and SCC $\\{3\\}$ is terminal."
"\n",
"However with this acceptance condition, we would be unable to extract only the strong behaviors: because that would require a way to disable the SCC $\\{0\\}$, and we cannot do that with this acceptance condition. This could be solved by adding a new acceptance set, but if we are about the modify the accepance condition, it seems wiser to simply it.\n",
"Our solution to this problem is that whenever an acceptance condition is always satisfiable, we consider the entire automaton as weak, and ignore all requests to extract the strong part. As a consequence, the output will always use B\u00fcchi acceptance."
] ]
}, },
{ {
@ -4786,7 +4783,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc0c2d50> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006f6c0> >"
] ]
}, },
{ {
@ -4874,7 +4871,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a450> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006fc60> >"
] ]
}, },
{ {
@ -4991,7 +4988,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8dcc11a450> >" "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f734006fc60> >"
] ]
} }
], ],