5488cb75c6
Previous output was not very usable in presence of decomposed specifications. We now keep track of the number of parts, and also prefix the columns names with "max_" or "sum_" to indicate how their statistics are updated in presence of multiple part. Other missing statistics, like the size of the translated automaton, or maximal number of colors seen in a game, have been added. * spot/twaalgos/synthesis.hh (bench_var): Rename, augment, and document each statistsic. * spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc, bin/ltlsynt.cc: Adjust to the new naming scheme. * doc/org/ltlsynt.org: Show a CSV file, and document its columns. * tests/core/ltlsynt-pgame.test, tests/core/ltlsynt2.test, tests/core/ltlsynt.test: Adjust test cases. * NEWS: Mention the backward incompatible change.
156 lines
3.6 KiB
Bash
Executable file
156 lines
3.6 KiB
Bash
Executable file
#! /bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) by the Spot authors, see the AUTHORS file for details.
|
|
#
|
|
# This file is part of Spot, a model checking library.
|
|
#
|
|
# Spot is free software; you can redistribute it and/or modify it
|
|
# under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation; either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
# License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
. ./defs || exit 1
|
|
|
|
set -e
|
|
|
|
# From SYNTCOMP
|
|
cat >aut7.hoa <<EOF
|
|
HOA: v1
|
|
name: "GFa | G(b <-> Xa)"
|
|
Start: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
AP: 2 "a" "b"
|
|
controllable-AP: 1
|
|
properties: explicit-labels trans-labels
|
|
--BODY--
|
|
State: 0
|
|
[t] 1
|
|
[1] 2
|
|
[!1] 3
|
|
State: 1 "GFa"
|
|
[0] 1 {0}
|
|
[!0] 1
|
|
State: 2 "a & G(b <-> Xa)" {0}
|
|
[0&1] 2
|
|
[0&!1] 3
|
|
State: 3 "!a & G(b <-> Xa)" {0}
|
|
[!0&1] 2
|
|
[!0&!1] 3
|
|
--END--
|
|
EOF
|
|
|
|
test UNREALIZABLE = `ltlsynt --realizability --from-pgame aut7.hoa`
|
|
|
|
grep -v controllable-AP aut7.hoa > aut7b.hoa
|
|
run 2 ltlsynt --realizability --from-pgame aut7b.hoa 2>stderr
|
|
grep 'aut7b.*controllable-AP' stderr
|
|
|
|
|
|
# From SYNTCOMP
|
|
cat >UnderapproxDemo2.ehoa <<EOF
|
|
HOA: v1
|
|
States: 4
|
|
Start: 0
|
|
AP: 4 "u0y0x" "u0y0y" "p0p0p0x" "p0p0p0y"
|
|
controllable-AP: 1 0
|
|
acc-name: parity max even 3
|
|
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
|
|
properties: trans-labels explicit-labels trans-acc colored complete
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0
|
|
[!0&1&2&!3 | 0&!1&2&!3] 1 {1}
|
|
[!0&1&!2&!3 | 0&!1&!2&!3] 0 {2}
|
|
[!0&1&3 | 0&!1&3] 2 {1}
|
|
[!0&!1 | 0&1] 3 {1}
|
|
State: 1
|
|
[!0&1&!3 | 0&!1&!3] 1 {1}
|
|
[!0&1&3 | 0&!1&3] 2 {1}
|
|
[!0&!1 | 0&1] 3 {1}
|
|
State: 2
|
|
[!0&1 | 0&!1] 2 {2}
|
|
[!0&!1 | 0&1] 3 {1}
|
|
State: 3
|
|
[t] 3 {1}
|
|
--END--
|
|
EOF
|
|
|
|
test UNREALIZABLE = `ltlsynt --realizability --from-pgame UnderapproxDemo2.ehoa`
|
|
|
|
# From SYNTCOMP
|
|
cat >starve.ehoa <<EOF
|
|
HOA: v1
|
|
name: "G(!r | Fg)"
|
|
States: 2
|
|
Start: 0
|
|
AP: 2 "r" "g"
|
|
acc-name: parity min odd 3
|
|
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
|
|
properties: trans-labels explicit-labels trans-acc colored complete
|
|
properties: deterministic stutter-invariant
|
|
controllable-AP: 1
|
|
--BODY--
|
|
State: 0
|
|
[!0 | 1] 0 {1}
|
|
[0&!1] 1 {2}
|
|
State: 1
|
|
[1] 0 {1}
|
|
[!1] 1 {2}
|
|
--END--
|
|
EOF
|
|
|
|
test REALIZABLE = `ltlsynt --realizability --from-pgame starve.ehoa`
|
|
|
|
cat >expect <<EOF
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 2 "r" "g"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
controllable-AP: 1
|
|
--BODY--
|
|
State: 0
|
|
[!0] 0
|
|
[0&1] 0
|
|
--END--
|
|
EOF
|
|
ltlsynt --from-pgame starve.ehoa >results
|
|
diff expect results
|
|
|
|
ltlsynt --realizability --from-pgame starve.ehoa \
|
|
--from-pgame UnderapproxDemo2.ehoa \
|
|
--from-pgame aut7.hoa --csv=out.csv >result || :
|
|
cat >expect <<EOF
|
|
REALIZABLE
|
|
UNREALIZABLE
|
|
UNREALIZABLE
|
|
EOF
|
|
diff result expect
|
|
cat out.csv
|
|
test 4 = `wc -l < out.csv`
|
|
|
|
ltlsynt --from-pgame starve.ehoa \
|
|
--from-pgame UnderapproxDemo2.ehoa \
|
|
--from-pgame aut7.hoa --csv-without-formula=out.csv >result || :
|
|
test 4 = `wc -l < out.csv`
|
|
cut -d, -f 1,2,7,8,9,10,11,12,13 <out.csv >right
|
|
REST=strat_states,max_strat_edges,max_simpl_strat_states,max_simpl_strat_edges
|
|
cat >expect <<EOF
|
|
source,split,realizable,max_game_states,max_game_colors,max_$REST
|
|
"starve.ehoa:1.1-18.7",auto,1,4,3,1,2,1,2
|
|
"UnderapproxDemo2.ehoa:1.1-25.7",auto,0,9,3,0,0,0,0
|
|
"aut7.hoa:1.1-23.7",auto,0,10,1,0,0,0,0
|
|
EOF
|
|
diff right expect
|