Merge branch 'master' into next
This commit is contained in:
Alexandre Duret-Lutz
commit
694e485ec2
4 changed files with 31 additions and 400 deletions
40
NEWS
40
NEWS
|
|
@ -1,4 +1,4 @@
|
||||||
New in spot 2.0a (not yet released)
|
New in spot 2.0.1a (not yet released)
|
||||||
|
|
||||||
Command-line tools:
|
Command-line tools:
|
||||||
|
|
||||||
|
|
@ -53,29 +53,35 @@ New in spot 2.0a (not yet released)
|
||||||
is_inherently_weak() will update the corresponding properties of
|
is_inherently_weak() will update the corresponding properties of
|
||||||
the automaton as a side-effect of their check.
|
the automaton as a side-effect of their check.
|
||||||
|
|
||||||
* twa::unregister_ap() and twa_graph::remove_unused_ap() are new
|
|
||||||
methods introduced to fix some of the bugs below.
|
|
||||||
|
|
||||||
Documentation:
|
|
||||||
|
|
||||||
* Add missing documentation for the option string passed to
|
|
||||||
spot::make_emptiness_check_instantiator().
|
|
||||||
|
|
||||||
* There is a now a spot(7) man page listing all installed
|
|
||||||
command-line tools.
|
|
||||||
|
|
||||||
Python:
|
Python:
|
||||||
|
|
||||||
* The tgba_determinize() function is now accessible in Python.
|
|
||||||
|
|
||||||
* The __format__() method for formula support the same
|
* The __format__() method for formula support the same
|
||||||
operator-rewritting feature introduced in ltldo and ltlcross.
|
operator-rewritting feature introduced in ltldo and ltlcross.
|
||||||
So "{:[i]s}".format(f) is the same as
|
So "{:[i]s}".format(f) is the same as
|
||||||
"{:s}".format(f.unabbreviate("i")).
|
"{:s}".format(f.unabbreviate("i")).
|
||||||
|
|
||||||
|
|
||||||
|
New in spot 2.0.1 (2016-05-09)
|
||||||
|
|
||||||
|
Library:
|
||||||
|
|
||||||
|
* twa::unregister_ap() and twa_graph::remove_unused_ap() are new
|
||||||
|
methods introduced to fix some of the bugs listed below.
|
||||||
|
|
||||||
|
Documentation:
|
||||||
|
|
||||||
|
* Add missing documentation for the option string passed to
|
||||||
|
spot::make_emptiness_check_instantiator().
|
||||||
|
|
||||||
|
* There is now a spot(7) man page listing all installed
|
||||||
|
command-line tools.
|
||||||
|
|
||||||
|
Python:
|
||||||
|
|
||||||
|
* The tgba_determinize() function is now accessible in Python.
|
||||||
|
|
||||||
Bug fixes:
|
Bug fixes:
|
||||||
|
|
||||||
* Typo in documentation of the -H option in --help output.
|
|
||||||
* The automaton parser would choke on comments like /******/.
|
* The automaton parser would choke on comments like /******/.
|
||||||
* check_strength() should also set negated properties.
|
* check_strength() should also set negated properties.
|
||||||
* Fix autfilt to apply --simplify-exclusive-ap only after
|
* Fix autfilt to apply --simplify-exclusive-ap only after
|
||||||
|
|
@ -93,12 +99,14 @@ New in spot 2.0a (not yet released)
|
||||||
(Note that it will also throw an exception if the automaton uses
|
(Note that it will also throw an exception if the automaton uses
|
||||||
an unregistered AP; this is how some of the above bugs were
|
an unregistered AP; this is how some of the above bugs were
|
||||||
found.)
|
found.)
|
||||||
* The for Small or Deterministic preference, the postprocessor
|
* For Small or Deterministic preference, the postprocessor
|
||||||
will now unregister atomic propositions that are no longer
|
will now unregister atomic propositions that are no longer
|
||||||
used in labels. Simplification of exclusive properties
|
used in labels. Simplification of exclusive properties
|
||||||
and remove_ap::strip() will do similarly.
|
and remove_ap::strip() will do similarly.
|
||||||
* bench/ltl2tgba/ was not working since the source code
|
* bench/ltl2tgba/ was not working since the source code
|
||||||
reorganization of 1.99.7.
|
reorganization of 1.99.7.
|
||||||
|
* Various typos and minor documentation fixes.
|
||||||
|
|
||||||
|
|
||||||
New in spot 2.0 (2016-04-11)
|
New in spot 2.0 (2016-04-11)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -21,7 +21,7 @@
|
||||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
AC_PREREQ([2.61])
|
AC_PREREQ([2.61])
|
||||||
AC_INIT([spot], [2.0a], [spot@lrde.epita.fr])
|
AC_INIT([spot], [2.0.1a], [spot@lrde.epita.fr])
|
||||||
AC_CONFIG_AUX_DIR([tools])
|
AC_CONFIG_AUX_DIR([tools])
|
||||||
AC_CONFIG_MACRO_DIR([m4])
|
AC_CONFIG_MACRO_DIR([m4])
|
||||||
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
|
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,8 @@
|
||||||
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil
|
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil
|
||||||
#+EMAIL: spot@lrde.epita.fr
|
#+EMAIL: spot@lrde.epita.fr
|
||||||
#+HTML_LINK_HOME: index.html
|
#+HTML_LINK_HOME: index.html
|
||||||
#+MACRO: SPOTVERSION 2.0
|
#+MACRO: SPOTVERSION 2.0.1
|
||||||
#+MACRO: LASTRELEASE 2.0
|
#+MACRO: LASTRELEASE 2.0.1
|
||||||
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.tar.gz][=spot-2.0.tar.gz=]]
|
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.1.tar.gz][=spot-2.0.1.tar.gz=]]
|
||||||
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0/NEWS][summary of the changes]]
|
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0-1/NEWS][summary of the changes]]
|
||||||
#+MACRO: LASTDATE 2016-04-11
|
#+MACRO: LASTDATE 2016-05-09
|
||||||
|
|
|
||||||
|
|
@ -588,381 +588,4 @@ State: 4
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
diff out expected
|
diff out expected
|
||||||
|
autfilt -q expected
|
||||||
# Test HOA v1.1
|
|
||||||
autfilt expected -H1.1 --check > out2
|
|
||||||
|
|
||||||
cat >expected2 <<EOF
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 2 "a" "b"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc !complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[1] 1
|
|
||||||
[0&!1] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 1
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[0] 1
|
|
||||||
[!0] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[0] 1
|
|
||||||
[!0] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 0
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[t] 1
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 4
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 1
|
|
||||||
[2] 2
|
|
||||||
State: 1
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 1
|
|
||||||
[!1&2] 2
|
|
||||||
[1&2] 3
|
|
||||||
State: 2 {0}
|
|
||||||
[t] 2
|
|
||||||
State: 3
|
|
||||||
[!1] 2
|
|
||||||
[1] 3
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 1
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored !complete
|
|
||||||
properties: deterministic stutter-invariant weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[!0] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 3
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc !complete
|
|
||||||
properties: !deterministic !unambiguous weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[0&1&!2] 1
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 2
|
|
||||||
State: 1 {0}
|
|
||||||
[0] 1
|
|
||||||
State: 2
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 2
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels trans-acc !complete
|
|
||||||
properties: deterministic stutter-invariant !inherently-weak
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 1
|
|
||||||
State: 1
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 1
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 2 "a" "b"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc !complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[1] 1
|
|
||||||
[0&!1] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 1
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[0] 1
|
|
||||||
[!0] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[0] 1
|
|
||||||
[!0] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 0
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[t] 1
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 1
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored !complete
|
|
||||||
properties: deterministic stutter-invariant weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[!0] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 5
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc !complete
|
|
||||||
properties: !deterministic !unambiguous weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[0&1&!2] 1
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 2
|
|
||||||
[2] 3
|
|
||||||
State: 1 {0}
|
|
||||||
[0] 1
|
|
||||||
State: 2
|
|
||||||
[!1&!2] 0
|
|
||||||
[1&!2] 2
|
|
||||||
[!1&2] 3
|
|
||||||
[1&2] 4
|
|
||||||
State: 3 {0}
|
|
||||||
[t] 3
|
|
||||||
State: 4
|
|
||||||
[!1] 3
|
|
||||||
[1] 4
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 1
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored !complete
|
|
||||||
properties: deterministic stutter-invariant weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[!0] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 3
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels trans-acc !complete
|
|
||||||
properties: !deterministic !unambiguous !inherently-weak
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[0&1&!2] 1
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 2
|
|
||||||
State: 1
|
|
||||||
[0] 1 {0}
|
|
||||||
State: 2
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 2
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 2 "a" "b"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc !complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[1] 1
|
|
||||||
[0&!1] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 1
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[0] 1
|
|
||||||
[!0] 0
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
Acceptance: 2 Inf(0) | Inf(1)
|
|
||||||
properties: trans-labels explicit-labels trans-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant inherently-weak !weak
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[0] 1 {1}
|
|
||||||
[!0] 0 {0}
|
|
||||||
State: 1
|
|
||||||
[t] 0 {0}
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 2
|
|
||||||
Start: 0
|
|
||||||
AP: 0
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored complete
|
|
||||||
properties: deterministic stutter-invariant terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[t] 1
|
|
||||||
State: 1 {0}
|
|
||||||
[t] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 1
|
|
||||||
Start: 0
|
|
||||||
AP: 1 "a"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels state-acc colored !complete
|
|
||||||
properties: deterministic stutter-invariant weak !terminal
|
|
||||||
--BODY--
|
|
||||||
State: 0 {0}
|
|
||||||
[!0] 0
|
|
||||||
--END--
|
|
||||||
HOA: v1.1
|
|
||||||
States: 5
|
|
||||||
Start: 0
|
|
||||||
AP: 3 "b" "a" "c"
|
|
||||||
acc-name: Buchi
|
|
||||||
Acceptance: 1 Inf(0)
|
|
||||||
properties: trans-labels explicit-labels trans-acc !complete
|
|
||||||
properties: !deterministic !unambiguous !inherently-weak
|
|
||||||
--BODY--
|
|
||||||
State: 0
|
|
||||||
[0&1&!2] 1
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 2
|
|
||||||
[2] 3
|
|
||||||
State: 1
|
|
||||||
[0] 1 {0}
|
|
||||||
State: 2
|
|
||||||
[!1&!2] 0 {0}
|
|
||||||
[1&!2] 2
|
|
||||||
[!1&2] 3
|
|
||||||
[1&2] 4
|
|
||||||
State: 3
|
|
||||||
[t] 3 {0}
|
|
||||||
State: 4
|
|
||||||
[!1] 3
|
|
||||||
[1] 4
|
|
||||||
--END--
|
|
||||||
EOF
|
|
||||||
|
|
||||||
diff out2 expected2
|
|
||||||
|
|
||||||
# Make sure no property are lost
|
|
||||||
autfilt -H1.1 out2 > out3
|
|
||||||
diff out3 expected2
|
|
||||||
|
|
||||||
|
|
||||||
test 2 = `autfilt -c --sccs=4 out`
|
|
||||||
test 5 = `autfilt -c --sccs=2 out`
|
|
||||||
test 1 = `autfilt -c -v --inherently-weak-sccs=1.. out`
|
|
||||||
test 2 = `autfilt -c --weak-sccs=2 out`
|
|
||||||
test 14 = `autfilt -c --terminal-sccs=1 out`
|
|
||||||
test 2 = `autfilt -c --terminal-sccs=1 --inherently-weak-sccs=2 out`
|
|
||||||
test 4 = `autfilt -c --rejecting-sccs=1 --accepting-sccs=1 out`
|
|
||||||
test 0 = `autfilt -c --trivial-sccs=1.. out`
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue