Commit bd739a57 authored by Maximilien Colange's avatar Maximilien Colange
Browse files

Heavily rewrite and optimize the determinization

* NEWS: document the rewrite
* spot/twaalgos/determinize.cc: lots of code optimizations
* tests/core/safra.test, tests/python/highlighting.ipynb,
  tests/python/simstate.py: Update tests
parent 308415f8
......@@ -132,6 +132,11 @@ New in spot 2.4.1.dev (not yet released)
https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html for
examples.
- Determinization has been heavily rewritten and optimized. The algorithm has
(almost) not changed, but it runs muuuch faster now. It also features an
optimization for stutter-invariant automata that may produce slightly
smaller automata.
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
This diff is collapsed.
......@@ -52,15 +52,15 @@ properties: trans-labels explicit-labels trans-acc deterministic
State: 0
[0] 1
State: 1
[0] 2 {1}
[!0&1] 3
[!0&1] 2
[0] 3 {1}
State: 2
[0] 1
[!0&1] 3
State: 3
[0&!1] 0
[0&1] 2
[!0&1] 3
[!0&1] 2
[0&1] 3
State: 3
[0] 1
[!0&1] 2
--END--
EOF
......@@ -98,19 +98,19 @@ State: 0
[0] 1
State: 1
[0&!1] 1
[0&1] 2
[!0&1] 3 {1}
[!0&1] 2 {1}
[0&1] 3
State: 2
[0&!1] 0
[!0&1] 2 {1}
[0&1] 3
State: 3
[0&1] 1 {1}
[!0&1] 3 {1}
[!0&1] 2 {1}
[0&!1] 4
State: 3
[0&!1] 0
[0&1] 2
[!0&1] 3 {1}
State: 4
[0] 1 {1}
[!0&1] 3 {1}
[!0&1] 2 {1}
--END--
EOF
......
This diff is collapsed.
......@@ -76,19 +76,19 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 "{₀[0]₀}"
[0&!1] 0 {1}
[!0&!1] 0
[!0&1] 0
[0&!1] 0 {1}
[0&1] 1 {3}
State: 1 "{₀[0]{₂[2]₂}₀}{₁[1]₁}"
[0&!1] 0 {1}
[!0&!1] 0 {2}
[!0&1] 2
[0&!1] 0 {1}
[0&1] 1 {3}
State: 2 "{₀[0]₀}{₁[1]₁}"
[0&!1] 0 {1}
[!0&!1] 0 {2}
[!0&1] 2
[0&!1] 0 {1}
[0&1] 1 {3}
--END--"""
......@@ -118,53 +118,53 @@ Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0 "{₀[0#0,0#1]₀}"
[!0&1] 1
[0&!1] 0
[0&1] 1
[!0&1] 2
State: 1 "{₀[0#0,0#1] [1#1]₀}"
[0&!1] 3
[0&1] 2
State: 1 "{₀[1#1]₀}"
[!0&1] 0
[0&!1] 3 {1}
[0&1] 4
[!0&1] 1
State: 2 "{₀[1#1]₀}"
[0&!1] 5 {1}
[0&1] 3
State: 2 "{₀[0#0,0#1] [1#1]₀}"
[!0&1] 2
[0&!1] 4
[0&1] 5
State: 3 "{₀[1#0]₀}"
[!0&1] 0
State: 3 "{₀[0#0,0#1]{₁[1#0]₁}₀}"
[0&!1] 3
[0&1] 6
State: 4 "{₀[0#0,0#1]{₁[1#0]₁}₀}"
[!0&1] 7
State: 4 "{₀[0#0,0#1] [1#1]{₁[1#0]₁}₀}"
[0&!1] 3
[0&1] 6
[0&!1] 4
[0&1] 8
State: 5 "{₀[0#0,0#1] [1#1]{₁[1#0]₁}₀}"
[!0&1] 7
State: 5 "{₀[1#0]₀}"
[0&!1] 5
[0&!1] 4
[0&1] 8
[!0&1] 0
State: 6 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}"
[0&!1] 8 {1}
[0&1] 9 {1}
[!0&1] 1 {1}
State: 6 "{₀[0#0,0#1] [1#0]₀}"
[!0&1] 2
[0&!1] 6
[0&1] 9
State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}"
[0&!1] 8 {1}
[0&1] 9 {1}
[!0&1] 10
State: 8 "{₀[0#0,0#1] [1#0]₀}"
[0&!1] 8
[0&1] 9
[!0&1] 1
[0&!1] 6 {1}
[0&1] 9 {1}
State: 8 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}"
[!0&1] 2 {1}
[0&!1] 6 {1}
[0&1] 9 {1}
State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}"
[0&!1] 3
[0&1] 4
[!0&1] 1
[!0&1] 2
[0&!1] 4
[0&1] 5
State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}"
[0&!1] 3 {3}
[0&1] 11
[!0&1] 7
[0&!1] 4 {3}
[0&1] 11
State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
[0&!1] 8 {1}
[!0&1] 2 {1}
[0&!1] 6 {1}
[0&1] 9 {1}
[!0&1] 1 {1}
--END--"""
a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')
......
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