Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
Spot
Commits
c0a845b2
Commit
c0a845b2
authored
Oct 01, 2013
by
Alexandre Duret-Lutz
Browse files
Release Spot 1.2.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.
parent
f48b5e50
Changes
3
Hide whitespace changes
Inline
Side-by-side
NEWS
View file @
c0a845b2
New in spot 1.
1.4a (not relased
)
New in spot 1.
2 (2013-10-01
)
* Changes to command-line tools:
...
...
@@ -63,8 +63,8 @@ New in spot 1.1.4a (not relased)
- ltl2tgba, ltl2tgta, and dstar2tgba can use a SAT-solver to
minimize deterministic automata. Doing so is only needed on
properties that are stronger than obligations (for
which our
WDBA-minimization procedure will return a minimimal
properties that are stronger than obligations (for
obligations
our
WDBA-minimization procedure will return a minimimal
deterministic automaton more efficiently) and is disabled by
default. See the spot-x(7) man page for documentation about the
related options: sat-minimize, sat-states, sat-acc, state-based.
...
...
@@ -156,11 +156,12 @@ New in spot 1.1.4a (not relased)
- When minimize_obligation() is not given the formula associated
to the input automaton, but that automaton is deterministic, it
can still attempt to call minimize_wdba() and check the correcteness
using dtgba_complement().
using dtgba_complement(). This allows dstar2tgba to apply
WDBA-minimization on deterministic Rabin automata.
- tgba_reachable_iterator_depth_first has been redesigned to
effectively perform a DFS. As a consequence, it does not
inherit
anymore
from tgba_reachable_iterator.
inherit from tgba_reachable_iterator
anymore
.
- postproc::set_pref() was used to accept an argument among Any,
Small or Deterministic. These can now be combined with Complete
...
...
@@ -171,6 +172,10 @@ New in spot 1.1.4a (not relased)
implication checks slightly. Also, literals are now sorted
using strverscmp(), so that p5 comes before p12.
- Syntactic implication checks have been generalized slightly
(for instance 'a & b & F(a & b)' is now reduced to 'a & b'
while it was not changed in previous versions).
- All the parsers implemented in Spot now use the same type to
store locations.
...
...
configure.ac
View file @
c0a845b2
...
...
@@ -20,7 +20,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.61])
AC_INIT([spot], [1.
1.4a
], [spot@lrde.epita.fr])
AC_INIT([spot], [1.
2
], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
...
...
doc/org/tools.org
View file @
c0a845b2
#+TITLE: Command-line tools installed by Spot 1.
1.4
#+TITLE: Command-line tools installed by Spot 1.
2
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment