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

partial_degeneralization: generalize to terms that contain todegen

Browse source 
* spot/twaalgos/degen.cc: Implement this.
* tests/python/pdegen.py: Add tests.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-04 13:47:44 +01:00
parent b733d486be
commit 8df616ee0d
2 changed files with 91 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

20
spot/twaalgos/degen.cc
View file

@ -767,12 +767,16 @@ namespace spot
SPOT_FALLTHROUGH;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
{
pos -= 2;
if (code[pos].mark != todegen)
tostrip -= code[pos].mark;
acc_cond::mark_t m = code[pos].mark;
if (todegen.subset(m))
m -= todegen;
tostrip -= m;
break;
}
}
}
while (pos > 0);
return tostrip;
}
@ -812,19 +816,23 @@ namespace spot
SPOT_FALLTHROUGH;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
if (code[pos].mark == todegen)
{
code[pos].mark = accmark;
pos -= 2;
acc_cond::mark_t m = code[pos].mark;
if (todegen.subset(m))
{
m -= todegen;
code[pos].mark = m.strip(tostrip) | accmark;
updated = true;
}
else
{
code[pos].mark = code[pos].mark.strip(tostrip);
code[pos].mark = m.strip(tostrip);
}
break;
}
}
}
while (pos > 0);
return updated;
}

68
tests/python/pdegen.py
View file

@ -212,3 +212,71 @@ pdaut9 = spot.partial_degeneralize(aut9, sets)
assert pdaut9.equivalent_to(aut9)
# one more state than aut9, because dualize completed the automaton.
assert pdaut9.num_states() == 10
aut10 = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 1 "p0"
Acceptance: 3 (Fin(0)|Fin(1))&Inf(2) | Inf(0)&Inf(1)
--BODY--
State: 0
[0] 1 {0}
State: 1
[0] 2 {2}
[!0] 2
State: 2
[0] 0 {1}
[!0] 1
--END--""")
pdaut10 = spot.partial_degeneralize(aut10, [0, 1])
assert pdaut10.equivalent_to(aut10)
assert pdaut10.to_str() == """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
Acceptance: 2 (Fin(1) & Inf(0)) | Inf(1)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0] 1 {1}
State: 1
[!0] 2
[0] 2 {0}
State: 2
[0] 0 {1}
[!0] 1
--END--"""
aut11 = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 1 "p0"
Acceptance: 4 (Fin(0)|Fin(1))&Inf(2) | Inf(0)&Inf(1)&Inf(3)
--BODY--
State: 0
[0] 1 {0}
State: 1
[0] 2 {2}
[!0] 2
State: 2
[0] 0 {1}
[!0] 1
--END--""")
pdaut11 = spot.partial_degeneralize(aut11, [0, 1])
assert pdaut11.equivalent_to(aut11)
assert pdaut11.to_str() == """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
Acceptance: 3 (Fin(2) & Inf(0)) | (Inf(1)&Inf(2))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0] 1 {2}
State: 1
[!0] 2
[0] 2 {0}
State: 2
[0] 0 {2}
[!0] 1
--END--"""