bin: handle '--parity=X --colored-parity' like '--colored-parity=X'
Fixes #602. * bin/common_post.cc (-P, -p): Do not overwrite an existing parity specification if none were given. * tests/core/parity2.test: Test this.
This commit is contained in:
parent
1dd2ce3ae2
commit
b6e782589e
2 changed files with 73 additions and 2 deletions
|
|
@ -231,7 +231,14 @@ parse_opt_post(int key, char* arg, struct argp_state*)
|
||||||
if (arg)
|
if (arg)
|
||||||
type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
|
type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
|
||||||
arg, parity_args, parity_types);
|
arg, parity_args, parity_types);
|
||||||
else
|
else if (!(type & spot::postprocessor::Parity))
|
||||||
|
// If no argument was given, we just require Parity.
|
||||||
|
// However, if a Parity condition was already set before,
|
||||||
|
// don't overwrite it. This way if someone mistakenly write
|
||||||
|
// `--parity='max even' --colored` without realizing that
|
||||||
|
// `--colored` is just the abbreviation for
|
||||||
|
// `--colored-parity=...` with the default argument, we
|
||||||
|
// won't reset the 'max even' setting.
|
||||||
type = spot::postprocessor::Parity;
|
type = spot::postprocessor::Parity;
|
||||||
if (key == 'p')
|
if (key == 'p')
|
||||||
colored = spot::postprocessor::Colored;
|
colored = spot::postprocessor::Colored;
|
||||||
|
|
|
||||||
|
|
@ -27,6 +27,18 @@ for x in P 'Pmin odd' 'Pmax even' p 'pmin odd' 'pmax even'; do
|
||||||
ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3
|
ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3
|
||||||
ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' |
|
ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' |
|
||||||
autfilt -D --name=%M --high "-$x" >>res4
|
autfilt -D --name=%M --high "-$x" >>res4
|
||||||
|
(
|
||||||
|
## --colored is normally short for --colored-parity=any
|
||||||
|
## But in case someone types something like
|
||||||
|
## --parity='max odd' --colored
|
||||||
|
## let's make sure we handle it like --colored-parity='max odd'.
|
||||||
|
echo "=== -$x ==="
|
||||||
|
ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
|
||||||
|
"-$x" --stats='%[]g'
|
||||||
|
echo "=== -$x --colored ==="
|
||||||
|
ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
|
||||||
|
"-$x" --colored --stats='%[]g'
|
||||||
|
) >> res5
|
||||||
done
|
done
|
||||||
|
|
||||||
cat >expected<<EOF
|
cat >expected<<EOF
|
||||||
|
|
@ -1423,6 +1435,58 @@ State: 4
|
||||||
EOF
|
EOF
|
||||||
diff expected4 res4
|
diff expected4 res4
|
||||||
|
|
||||||
|
cat >expected5 <<EOF
|
||||||
|
=== -P ===
|
||||||
|
co-Buchi
|
||||||
|
Buchi
|
||||||
|
Rabin 1
|
||||||
|
=== -P --colored ===
|
||||||
|
parity max even 2
|
||||||
|
Streett 1
|
||||||
|
parity min odd 3
|
||||||
|
=== -Pmin odd ===
|
||||||
|
co-Buchi
|
||||||
|
Rabin 1
|
||||||
|
Rabin 1
|
||||||
|
=== -Pmin odd --colored ===
|
||||||
|
Rabin 1
|
||||||
|
parity min odd 3
|
||||||
|
parity min odd 3
|
||||||
|
=== -Pmax even ===
|
||||||
|
parity max even 2
|
||||||
|
Buchi
|
||||||
|
parity max even 2
|
||||||
|
=== -Pmax even --colored ===
|
||||||
|
parity max even 2
|
||||||
|
parity max even 3
|
||||||
|
parity max even 4
|
||||||
|
=== -p ===
|
||||||
|
parity max even 2
|
||||||
|
Streett 1
|
||||||
|
parity min odd 3
|
||||||
|
=== -p --colored ===
|
||||||
|
parity max even 2
|
||||||
|
Streett 1
|
||||||
|
parity min odd 3
|
||||||
|
=== -pmin odd ===
|
||||||
|
Rabin 1
|
||||||
|
parity min odd 3
|
||||||
|
parity min odd 3
|
||||||
|
=== -pmin odd --colored ===
|
||||||
|
Rabin 1
|
||||||
|
parity min odd 3
|
||||||
|
parity min odd 3
|
||||||
|
=== -pmax even ===
|
||||||
|
parity max even 2
|
||||||
|
parity max even 3
|
||||||
|
parity max even 4
|
||||||
|
=== -pmax even --colored ===
|
||||||
|
parity max even 2
|
||||||
|
parity max even 3
|
||||||
|
parity max even 4
|
||||||
|
EOF
|
||||||
|
diff expected5 res5
|
||||||
|
|
||||||
ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
|
ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
|
||||||
'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
|
'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
|
||||||
-f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'
|
-f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue