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

print_hoa: output all registered APs

Browse source 
Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
so that the methods where this behavior is expected can be fixed.

And fix ltsmin::kripke() which did not register APs.

Part of #170.

* spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
Throw an exception when printing automata using unregistered APs.
* spot/ltsmin/ltsmin.cc: Call register_ap().
* spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
New methods.
* spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
* tests/core/maskacc.test, tests/core/maskkeep.test,
tests/core/strength.test: Adjust expected results.
* NEWS: Mention those changes.
This commit is contained in:
Alexandre Duret-Lutz 2016-04-30 23:54:31 +02:00
parent dad17b36b8
commit a1b3b065fa
14 changed files with 111 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

6
tests/core/maskacc.test
View file

@ -1,7 +1,7 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -95,7 +95,7 @@ cat >expect3 <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic

4
tests/core/maskkeep.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -50,7 +50,7 @@ cat >expect1 <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic

30
tests/core/strength.test
View file

@ -293,26 +293,26 @@ State: 1 {0}
HOA: v1
States: 4
Start: 0
AP: 2 "a" "c"
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
--BODY--
State: 0
[!0&!1] 0
[0&!1] 1
[1] 2
[!1&!2] 0
[1&!2] 1
[2] 2
State: 1
[!0&!1] 0
[0&!1] 1
[!0&1] 2
[0&1] 3
[!1&!2] 0
[1&!2] 1
[!1&2] 2
[1&2] 3
State: 2 {0}
[t] 2
State: 3
[!0] 2
[0] 3
[!1] 2
[1] 3
--END--
/******************************/
HOA: v1
@ -349,17 +349,17 @@ State: 2
HOA: v1
States: 2
Start: 0
AP: 2 "a" "c"
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0&!1] 0 {0}
[0&!1] 1
[!1&!2] 0 {0}
[1&!2] 1
State: 1
[!0&!1] 0 {0}
[0&!1] 1
[!1&!2] 0 {0}
[1&!2] 1
--END--
/******************************/
HOA: v1