News

LTSmin: We have moved to github

Added by Jeroen Meijer over 2 years ago

SpinS: We have moved to github!

Added by Jeroen Meijer over 2 years ago

JTorX: Solution for Anidot problem on 64-bits linux

Added by Axel Belinfante about 3 years ago

When you run JTorx on 64-bits linux, the anidot animation/visualization may not work, because a 32-bit library, that anidot depends on, is not present on your system.
In that case, the textual output that appears in the window in which you started JTorX, will contain a message that libjpeg.so.62 could not be found or loaded.

In that case, the solution is to install that library.
On a system on which apt-get is used for installing software, the necessary commands are:

sudo apt-get update
sudo apt-get install libjpeg62:i386

JTorX: JTorX v1.11.2

Added by Axel Belinfante over 3 years ago

Changes w.r.t. JTorX v1.11.1:

Bug fixes:
  • made guidance work again (broken since v1.11.0)
  • when user closes/deletes JTorX window, immediately exit, even when a test run is active (do not wait until the quiescence timer expires)

JTorX: JTorX v1.11.1

Added by Axel Belinfante over 3 years ago

Changes w.r.t. JTorX v1.11.0:

Bug fixes:
  • avoid hang/crash when stopping a test run while auto mode is active
  • avoid hang/crash when exiting/quitting/dismissing JTorX while a test run (in auto mode) is active

JTorX: JTorX v1.11.0

Added by Axel Belinfante over 3 years ago

Changes w.r.t. JTorX v1.10.0-beta8:

New features:
  • added option to synthesize delta labels for states on tau-loops
  • added option to extend this by cloning states on tau-loops, where the clones have neither output nor internal actions
  • add special case for infinite guidance information
  • angelic completion button is now hidden
  • added tool tips to most GUI items
  • added support to use Graphml edge label position info in automaton visualisation (by default disabled, because it does not look nice, obviously we are missing something)
  • added Settings pane (where we now only have an option to enable use of edge label position information)
  • add torx-explorer timing information to the test run log
Bug fixes:
  • avoid printing stack traces in some situations
  • made automaton visualisation work on Mac OS X (mountain) lion and mavericks
  • in non-gui mode, do not print first menu of possible stimuli and expected responses
  • when translating LOTOS-style labels, ignore whitespace
  • deal with whitespace in labels in graphml(?)
  • make finding of start-state in graphml file work (again?) in certain situations(?)
  • recognize when a (symbolic) torx-explorer indicates that it is not able to determine whether a guard can be satisfied
  • when quiescence is observed, and for one or more output actions, satisfiability of the guard could not be determined, the guard(s) is/are incorporated in the test run log, and a conditional verdict is given at the end of the run
  • dialog box for saving an LTS now has a relevant set of file suffixes
  • reduced font size in automaton visualisation on linux, so it is now better readable
  • changed 'run' numbers to start at 1 (instead of 0) (shown in experimental coverage info), so run numbers coincide with numbers on Log... tabs
  • for Mac OS X mavericks: fix the left-most progress bar to not continuously show 'activity in progress'

JTorX: anidot visualization updated for Mac OS X (Mountain) Lion

Added by Axel Belinfante about 4 years ago

The anidot automaton visualization component has been updated to work out-of-the-box on Mac OS X 10.7 Lion and 10.8 Mountain Lion.
(and it should still work on Mac OS X 10.6 Snow Leopard).

This is available in the Files section as JTorX-1.9.4-ml.dmg and JTorX-1.10.0-beta8-ml.dmg.
Only the anidot component has been updated -- otherwise, these are identical to JTorX-1.9.4 resp. JTorX-1.10.0-beta8.

If earlier you got, on a Mac OS X computer, the error that the dotnew command is not available, then running the updated version should fix this.

Thus, we no longer need the additional dependency for Mac OS X 10.8 (Mountain Lion), for the anidot automaton visualization.

LTSmin: LTSmin 2.0

Added by Alfons Laarman over 4 years ago

Major changes (see also extract from NEWS file below):
  • Code refactor / reorganization
  • Multi-core BDD package Sylvan
  • New frontend for timed Uppaal models
  • New frontend for PBESs
  • Symbolic parity game solver
  • New multi-core LTL algorithms
  • New lockless data structures for state compression
  • Support for Mcrl/Mcrl2/PBES in the multi-core backend
  • SpinJa renamed to SpinS and extended with partial order reduction
  • Test suite based on DejaGnu

JTorX: JTorX v1.10.0-beta8

Added by Axel Belinfante almost 5 years ago

Changes to the STS library, identical to those in JTorX v1.9.4 (STS support jar files are built from stsimulator svn revision 344)
+ one additional bug fix

Bug fixes:
  • when checking for divergence that is caused by tau-loops is enabled, add all states on tau loop as target of delta
  • allow very short model/guide/impl file names (could crash on names with < 3 characters)
New features:
  • extended logging: capture all A_LOG lines from torx-explorer and torx-adapter to log
  • print SUBEDGENAME lines to log, containing id's of tau transitions leading to current (Tester) state
    (when for such transition no id is known, a '_' (underscore) is printed)
    curently, the items in the SUBEDGENAME are sorted using natural sorting order;
    for efficiency reasons it would be better to let such sorting be done by the program that analyzes the log

JTorX: JTorX v1.9.4

Added by Axel Belinfante almost 5 years ago

Identical to v1.9.3, except for changes in STS library; the jar files included are built from stsimulator svn revision 344.
+ one additional bug fix

Bug fixes in STS support (in stsimulator) :
  • fix bug in + operation on doubles (stsimultor svn revision 336)
  • fix bug in handling of unobservable (tau) actions (stsimulator revision 337)
Additional bug fix:
  • allow very short model/guide/impl file names (could crash on names with < 3 characters)

Extended code in STS support that extracts name-value bindings for the interaction variables from switch restrictions (guards) combined with valuation of location variables.

The STS support jar files now contain the svn revision number in the Manifest; this numbers is also show (on standard error) when the stsimulator (STS support) is started.

1 2 3 ... 5 Next ยป

Also available in: Atom