Skip to content

Version 1.1
Compare
Choose a tag to compare
@nmacedo nmacedo released this 30 Apr 15:16
· 224 commits to master since this release
v1.1
dbef7f6

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
Assets 2
Loading