Activity

From 17 Aug 2013 to 15 Sep 2013

15 Sep 2013

22:04 Revision 4e60d638: Improve libDDD detection
Alfons Laarman
22:04 Revision de53c403: Fix workspace metadata (use available JDK)
Alfons Laarman
22:03 Revision 2690ed3a: Update documentation
Alfons Laarman
21:45 Revision dbf6a7cc: Better bash completion script
Alfons Laarman
18:18 Revision 5d22bdb5: Update Bash completion script :)
Alfons Laarman
18:18 Revision a1b68f20: Hide development options
Alfons Laarman
16:31 Bug #723: Move invariant detection into POR layer
It may not be necessary to create a fake transition for the invariant, as it adds nothing to the results of the POR a... Alfons Laarman
14:00 Feature #724 (Assigned): Support better LTL to Buchi solutions
LTL3Buchi can be integrated (as in divine)
Spot also contains better algorithms.
LTL2Buchi should still stay avai...
Alfons Laarman

11 Sep 2013

19:08 Revision a0471a2b: Add deletion algorithm
Alfons Laarman

06 Sep 2013

01:15 Revision 91f860dc: Fix compilation warnings
Alfons Laarman
00:15 Revision e388dd9d: Merge branch 'al/next/por' into next
Conflicts (fixed):
src/pins-lib/pins.c
src/pins2lts-dist/pins2lts-dist.c
Alfons Laarman
23:33 Revision abf1c8f9: Add weak POR key transition check
Alfons Laarman
21:14 Revision 9a0e45fd: Fix pre-configure warnings
Alfons Laarman
21:13 Revision a632b92c: Small fixes in test suite
Alfons Laarman
21:13 Revision 1b4d38cf: Fix compilation warnings of Gijs and Stefan
Alfons Laarman
15:00 Revision cd6619a3: Fix deadlock in distributed runtime.
Stefan Blom
14:53 Revision e58aba4a: extra buffering for self calling tasks
Stefan Blom
14:53 Revision b6c2fcb2: compute and write traces to deadlocks
Stefan Blom
14:53 Revision 728b10c7: added trace computation for pins2lts-dist
Stefan Blom
14:53 Revision 1d056ed9: Enforce priorities on task queues and add buffered tasks.
Stefan Blom
14:53 Revision 31ad8e88: fix scoop for ghc 7.6.3
Stefan Blom
14:53 Revision 489e0197: Fix several indexing bugs, causing problem with traces found by symbolic tool.
Stefan Blom
14:53 Revision 7f00b149: fix plugin tool man pages
Stefan Blom
14:53 Revision ad5b6673: Add mapa language module
Stefan Blom
14:53 Revision b4b7c76f: Extend plugin loader.
1. Headers are now installed.
2. A library containing a single model can be loaded.
Stefan Blom
14:53 Revision fa8c83df: select trace from multi-trace file
Stefan Blom
14:53 Revision c51e6c59: extend bfs_reorder to allow unrachable parts
Stefan Blom
14:53 Revision be949be3: remove superfluous initial state count check
Stefan Blom
14:53 Revision c2f2c2fb: [lts-io] improve error messages
Stefan Blom
14:53 Revision 48deea16: extension of Prism TRA import
Stefan Blom
14:53 Revision ad492471: Add (deep) copy function for LTS, fix label getter
Stefan Blom
14:53 Revision 602e37ad: fix makefiles
Stefan Blom
14:53 Revision 2debbbfc: Add support for probabilistic LTSs.
1. Move rationals from lts-lib to util-lib for scoop
2. Write support for IMCA file format
3. Generic static analysis...
Stefan Blom
14:53 Revision 66d2fc6e: add access function for state labels
Stefan Blom
14:34 Revision a6f6a057: Add plugin language module.
Stefan Blom
14:32 Revision aac7634d: Merge branch 'maint' (including sb/maint) into next
Alfons Laarman
14:27 Revision 16efea6f: Merge branch 'sb/maint' into maint
Alfons Laarman
14:02 Revision 9d20eecf: Optional weak stubborn sets using a new commutes matrix
With SpinS update
TODO: fix NDS selection
Alfons Laarman
14:01 SpinS Revision 442f750f: New Action Commutes matrix (for weak stubborn sets)
Alfons Laarman
13:50 Revision 22c896dd: fix deadlock in MPI runtime
Stefan Blom
13:19 Revision 76fffbb3: fix GCF buffer overflow for many small sub-streams
Stefan Blom
13:18 Revision 8c0cdc29: Fix incorrect exit code when children are killed.
Stefan Blom
02:29 Revision e69a9b25: Weak stubborn sets
TODO: modify SpinS to not include NDS in DNA Alfons Laarman
02:05 Revision dba2d49c: Small code path optimization (algorithmic backend may reset flag)
Alfons Laarman

05 Sep 2013

00:50 Revision d1524803: Update SpinS
Improved DNA code, fully verified with POR check layer Alfons Laarman
00:46 SpinS Revision 86d064e7: Update gitignore
Alfons Laarman
00:31 Revision abfc8005: Print PINS DNA matrix
Alfons Laarman
00:30 Revision dd0e9637: Fix "empty frame" overflow in POR check and improve output
Alfons Laarman
00:28 SpinS Revision 1fe00ab0: Fix error in DNA due to uncleared cache
Alfons Laarman
23:24 SpinS Revision 4e8df24d: Improve DNA check
Alfons Laarman
22:42 Revision 31de6d5a: Fix stupid bug mixing LTL and safety provisos
Alfons Laarman
19:30 Revision 1676ee53: Updated POR tests with the insight that invariant counts are not preserved
Alfons Laarman
19:26 Revision 83f0e100: Relax POR for safety properties
- Disable visibility proviso (while still
recording visible transitions / labels)
- Implement safety proviso, by se...
Alfons Laarman
16:21 Bug #723 (Resolved): Move invariant detection into POR layer
By adding the invariant as a fake transition (which has as guard the invariant itself and as action an identity funct... Alfons Laarman
16:10 Feature #722 (New): Refine PINS transitions as seperate guards and actions
Currently, PINS is defined on the level of transitions.
The new POR layer already exposes the internals of these obj...
Alfons Laarman
15:59 Feature #680: PINS state and label manipulation functionality
My latest POR branch contains a pins-util.ch files with some initial PINS helper functions Alfons Laarman
15:58 Feature #712: Tracing for distributed tools
Hallo Lars,
In de git repository: http://www.cs.utwente.nl/~sccblom/git/ltsmin/
staat een branch 'sb/next' met da...
Alfons Laarman

03 Sep 2013

11:31 Revision d5a9b0ff: Made C++11 standard the default. The previous script did suffice,
because the AC_CHECK_HEADER macro has different behaviour in different
versions of autoconf: older versions of autoco...
Gijs Kant

31 Aug 2013

02:42 Revision 85b14ebc: Fix test code
Alfons Laarman
02:40 Revision 358bdb48: Fix compilation warnings
Alfons Laarman
02:29 Revision 5ea27ec9: Updated test suite for new POR results
Alfons Laarman

30 Aug 2013

18:47 Revision eed9fa77: Improve result print on stdout
Alfons Laarman
18:47 Revision dd8afeae: Fix progress transitions
Alfons Laarman
18:47 Revision 89855ece: Fix DFS_FIFO with POR
Alfons Laarman
18:47 Revision a9b36e21: Add deprecated warning to DVE POR dependency loader
Alfons Laarman
18:47 Revision 94886282: Refined visibility heuristic
Alfons Laarman
18:47 Revision 66d9ed7f: Fix heuristic for --no-V and L1/L2 check for --no-dynamic-labels
Alfons Laarman
18:47 Revision 8c402518: No heuristic, prefer dns, random and dynamic random POR
Alfons Laarman
18:47 Revision f7a17954: Extend POR check with NS search path printing
Alfons Laarman
18:47 Revision 35e51c43: Valmari's SCC-based algorithm (incomplete)
Alfons Laarman
18:47 Revision 3b7f33ea: Add Valmari's L1 / L2 proviso
* fixes bug in previous cycle implementation (emit all remaining didn't work)
* L1 proviso is discarded iff S proviso...
Alfons Laarman
18:47 Revision 3f306e9c: Refactored code
Fixed bug: dynamic visibilities were reset before L1/L2 check Alfons Laarman
18:47 Revision a1d85d84: Optimized init code
Alfons Laarman
18:47 Revision 7b955b08: SpinS with full DNA
Alfons Laarman
18:47 Revision d31ee5fb: Add Valmari's V proviso
Alfons Laarman
18:47 Revision c6f53298: Reintroduced NDS (with separate MCE from NDA)
* Moved popt into LTL / POR layers (TODO test)
* Noted difficult contract tools/por_proviso (TODO document)
Alfons Laarman
18:47 Revision fe865605: Removed NDS, fix DNA
Alfons Laarman
18:47 Revision 92b5748e: Extend POR check with check for disabled transitions
Alfons Laarman
18:47 Revision 37753c00: Improved matrix printing
-v prints POR matrices Alfons Laarman
18:47 Revision 08ba735f: POR check algorithm adapted to the new interface
Alfons Laarman
18:47 Revision 38e7c60a: Redesigned POR PINS interface
* MCE G X G --> !accords T X T
* NDS --> !MCE + NDS
The new definitions are analogous to the ones found in Valmari's...
Alfons Laarman
18:47 Revision 8384232f: Fix SpinS NESs
Alfons Laarman
18:47 Revision 35f8974d: Dynamic visibility
TODO all labels as guards in POR layer Alfons Laarman
18:47 Revision 625e0388: Implement POR cycle proviso for safety properties
* a proviso method is forced when invariants and actions are being detected
* if no proviso is present, the tools set...
Alfons Laarman
18:47 Revision 9cb19b3c: Improved color proviso
* The POR layer presets por_proviso for states that
are fully expanded. This can be used in the color
proviso to mark...
Alfons Laarman
18:47 Revision f943488f: Separate POR check layer in separate file
Alfons Laarman
18:47 Revision 7d66de77: pins2pins-por check persistent set
Elwin Pater
18:47 Revision d7b24e10: pins2pins-por check persistent set via commutativity
of persistent-set with non-persistent set.
Now POR is verified independent of the dependencies.
Alfons Laarman
18:47 Revision ac00e43b: Add MCE && Dependent check
Alfons Laarman
18:47 Revision f69209e0: Fix NES for atomics
Alfons Laarman
18:47 Revision a47c258a: Simplified POR layer
Alfons Laarman
18:27 Revision 4ee5eee2: Add tests for POR and DFS_FIFO
Alfons Laarman
15:56 Revision 1c6c429d: Remove end label visibility for deadlocks
Alfons Laarman
15:54 Revision f25c0543: Fix spins not found (Closes #719)
Alfons Laarman
15:54 Revision c5a3ccc3: Elaborate on reserved value in tree
Alfons Laarman
15:54 Revision 5415e7d3: Fix linking on linux
Alfons Laarman
15:54 Revision 97a5bfe4: Fix compilation warning in LTL semantics
Alfons Laarman
15:54 Revision b3db87f2: Fix predicate semantics implementation and improved error output from parser
Alfons Laarman

26 Aug 2013

16:55 Revision 06e56b3a: Patches by Jeroen Keiren.
Fixed linking errors on some compilers (initialisation of private static members),
links to certain new mcrl2 librari...
Gijs Kant
 

Also available in: Atom