Skip to content

v4.9

Latest
Latest
Compare
Choose a tag to compare
@davexparker davexparker released this 11 Aug 10:39
· 5 commits to master since this release
v4.9
08457fb

  • Explicit engine improvements

    • support for actions and transition rewards in Markov chains

  • Export functionality

    • export of exact and parametric models
    • preliminary DRN (Storm) output
    • multiple -exportmodel switches allowed
    • options for -exportmodel: format/actions/header/precision
    • export of Markov chain actions
    • remove old options (MRMC format, unordered, spy)
    • align -exportstrat and -exportadv switches

  • Model import functionality (from explicit files)

    • import of transition rewards
    • import for exact mode, LTSs
    • import progress display (symbolic engine)
    • import directly to sparse classes in explicit engine
      (now assume ascending states/choices in .tra files)

  • Minor modelling language updates

    • new power operator a^b, equivalent to pow(a,b)
    • fix: implication (=>) is right-associative

  • New/improved functionality

    • simplified/updated LTL-to-automaton scripts
    • simulator can take a random seed (API only)
    • exact model checking supported from GUI
    • optimal strategy synthesis for Rmax=? [ C ] (explicit)

  • Various bugfixes

  • Development and code-level changes

    • prism.Prism API: new/updated model export methods
    • prism.Prism API: remove some old deprecated methods
    • prism.Prism: refactored storage/access for model info
    • prism.Prism: integration of exact model building/checking
    • improved access to actions and their indices in models
    • redesign/refactoring of explicit engine reward classes
    • refactoring of explicit engine model import/export code
      (centralised in io package, export moved from model classes)
    • parametric engine refactored to use explicit models/rewards
    • refactoring of (explicit engine) interval model storage
    • symbolic code rearranged (new symbolic package)
    • symbolic model storage refactored, simplified, documented
    • extension of strategy classes, especially for induced models
    • Java-based symbolic-to-explicit model conversion
    • prism-auto: --errors-only switch

  • [More minor development and code-level changes]

    • explicit engine product construction refactoring
    • explicit model refactoring (infoString etc.)
    • default implementation of getVarDeclarationType in ModelGenerator
    • POMDP observation info storage refactoring
    • Expression.toString() respects operator precedence
    • VarList aware of EvaluationContext/EvalMode
    • parametric engine: improved error reporting and formatting
    • prism.API: exportprism moved from setting to API call
    • model export refactoring, including ModelExportTask
Assets 6
Loading