Version 1.2.4

Minor:

• guarantees the same order on relations for predictable results
• fixed a bug when all bounds static but temporal formula
• fixed a bug on automatic static/var bound splitting
• tests, documentation updated

Version 1.2.3

Major:

• support for alternative target-oriented strategies (#46)

Minor:

• Reverted iteration semantics, resets prefixes if coming from longer iterations
• Improved reporting from electrod

Version 1.2.2

Minor:

• Changes to the instance to formula translation (no quantification for ints, allow restriction of univ)
• Forbid iteration when set of changing formulas is empty
• Fixed the pretty printing of primed expressions
• Fixed a bug on the generation of the state-wise symmetry breaking predicate
• Additional tests for state-wise symmetry breaking predicate

Version 1.2.1

Minor

• Reverted support for integers in electrod
• Fixed multiple synchronisation bugs when iterating under decomposed strategy
• Fixed an assertion testing solver compatibility
• Fixed unsat cores for trivially unsat problems
• Fixed reporting during the temporal translation of sub-formulas (was causing unsat cores to be incomplete, #41)
• Fixed a reporting bug in decomposed solving without iteration
• Fixed a bug when number of configs an exact multiple of batch size in decomposed strategy
• Pulled a missing change from NoOverflows Kodkod that was not reseting the environment

Version 1.2

Features

• support for advanced SAT iteration operations, distinction between configuration and path iteration
• support for advanced iteration operations for decomposed strategy
• support for unsat cores for temporal formulas
• support for bounded model checking with the electrod backend
• disabled iteration through formulas for non SAT backend

Minor

• iteration implemented at the SAT level
• fixed a bug on the releases translation
• fixed a bug when translating constants under unrolled traces
• fixed a bug when evaluating past expressions
• better handling of unsupported features of different backends
• better reporting of stats for iterative temporal and decomposed solving
• travis integration
• updated temporal operators nomenclature (before, after, releases, triggered)
• decomposed strategy no longer automatically iterates over integrated problems, not compatible with new operations
• alternative instance encoding with some-disj pattern
• support for electrod 0.7.1

Version 1.1

Major changes:

• proper past semantics through loop unrolling
• proper temporal instance iteration
• instances assumed to always be infinite
• evaluator for instances from unbounded engined
• skolems not considered part of temporal instances
• properly terminates electrod processes

Full description:

• two alternative encodings for the unrolling of formulas with past operators, one with explicit unrolls and another implicit
• unified relation hierarchy with that of Alloy5, easier to identify relations as atoms, skolems and variable
• atom relations are ignored during symmetry breaking
• unified representation for temporal instances from bounded/unbounded engines
• the previous enables the evaluator on instances from the unbounded engine
• formulas and int expressions can also be evaluated at particular instants
• the evaluation of temporal instances relies on the original universe of the bounds
• assumed temporal instances always loop, simplified translation and bounds accordingly
• two alternative encodings for temporal iteration, one reifies atoms the other uses the some-disj pattern
• in the reification process atom relations are ignored during symmetry breaking
• in the formulation of instances, relations not mentioned in the formula are ignored
• an optimised iteration procedure for the bounded engine that acts directly on SAT
• fixed the translation of symbolic bounds to invert bounds for "difference" expressions
• termination of electrod processes properly terminates children smv processes
• skolem variables are not translated back into temporal instances, nor considered during iteration (but are still used for performance purposes)
• fixed a bug when expanding constants where state atoms would become part of the universe
• fixed a bug when slicing formulas with extra relations (eg, created during trivial iteration)
• fixed a bug when slicing single conjunct formulas
• added support for skolems at electrod (protected symbol $)
• added missing neq method to integer expressions
• fixed bug on running non-decomposed with decomposed bounds
• iteration for trivial solutions simplified
• fetched no overflow fixes from Alloy5
• solving engines now register whether unbounded
• pmaxsat yices disabled due to unpredictable results
• fixed a bug on symbolic bounds for static relations depending on variable ones+
• rename identifiers that are protected keywords in electrod