Skip to content

Version 2

Latest
Latest
Compare
Choose a tag to compare
@xblahoud xblahoud released this 23 Oct 17:57
· 14 commits to master since this release
v2.0.0
5c9c0c8

Version 2 brings a new interface and a lot of new functionalities, including new solvers, integration with Storm(py), strategies and simulator, and more.

Added

  • Solvers that use heuristics for strategies usable in control. This is implemented in class
    GoalLeaningES of the energy_solver.py module. See tut/Solvers
    notebook for more details. Use [nbviewer] for the rendered notebook if you don't want
    to run the notebook locally; it renders the animations correctly.
  • Support for full-featured strategies that resolve the next action to play based on the history. See Strategy
    for the interface. See tut/Strategies for more details.
    • CounterStrategy implements strategies with a limited memory. The class only
      maintains the energy level of the play and can use it for the selection of next
      actions. The class only implements the memory and relies on selector objects
      to choose the next action. Any object implementing select_action(state, energy)
      can be used as selector.
    • CounterSelector is an enriched variant of what was called "strategy" in
      versions up to 1.2. This is the class intended to be used by the
      CounterStrategy instances.
    • SelectionRule is a helper class that stores the selection rules for one
      state. It is basically a dict enriched with select_action (and update)
      function. The keys in this dict are lower bounds of intervals that are
      mapped to the corresponding values. select_action takes care of the
      translation of lower bounds to intervals.
  • Integration with Stormpy for reading PRISM and Storm models into FiMDP and for
    translation of FiMDP models into equivalent models in Stormpy. See
    tut/Storm_and_prism for more details.
  • Ability to reason about Consumption MDPs with state labeled by sets of atomic propositions.
    This is implemented in the module labeled.py. The labeled ConsMDPs can be checked against
    specifications given by deterministic DBAs or the recurrence fragment of LTL. This requires
    [Spot] to be installed. See tut/Labeled for more details.
  • Binary search for detection of minimal capacity needed for a task
    (function mincap_solvers.bin_search).
  • fimdp.setup() configures FiMDP to create nicer pictures of ConsMDPs.
  • Solvers can now be visualized. Legend for the semantics of the minimal levels can be
    requested by calling solver.show(.l)
  • Show now takes <N option where the integer N marks the maximal number of states that
    should be drawn. It can be also specified by max_states=N.
  • ConsMDP.show takes targets argument which enables to highlight the given
    set of targets. Alternatively, targets can be specified using the option
    string ".T{t₁,t₂,...}". This cannot be used for solvers.

Changed

The package underwent a massive refactoring. There is a completely new interface for
energy solvers, part of the ConsMDP interface was removed (in favor of solvers), and
most of the codes was moved to new (or renamed) modules. The changes are listed below
and split into backward-incompatible and -compatible.

Backward incompatible changes

  • ConsMDP class does no longer have functions get_buchi and similar. Instead,
    solvers must be used explicitly. Moreover, they have no solver associated anymore
    and when visualized, they never show minimal levels for objectives (visualize solver
    instead).
    See [tut/Basics][Basics] for more details.
  • Solvers have new interface. See the corresponding
    issue #29 or the [Basics] notebook
    for more details.
  • moved between modules:
    • The class ConsMDP and its helper classes (ActionData and iterators) are moved
      from consMDP.py module to core.py.
    • Code regarding explicit encoding of energy to state-space was moved to explicit.py
    • Fixpoints-related code was moved to energy_solvers.py
    • Objectives definitions (BUCHI, etc.) moved to objectives.py
  • energy_solver.py renamed to energy_solvers.py
  • The update function of energy solvers now stores pointer to the whole ActionData object instead of
    just label. Add .label to every access to actions stored in the current representations
    of strategies.

Backward compatible changes

  • EnergySolvers.get_strategy returns CounterSelector objects instead of list of dicts
  • ActionData.__repr__ now prints full information about the action (source state, consumption, label, and successor distribution).
  • Visualization uses various shapes where appropriate.
Assets 2