Pint 2019-05-24

New features:

• pint-reach --quick performs only the over-approximation (results only in False or Inconc)

Bugfixes:

• the reachability continuity computation contained a bug that can lead to wrong results with over-approximation of reachability with non-binary automata networks

Building:

• Switch to Zarith OCaml library (instead of deprecated Nums)

Pint 2018-11-30

Improvements:

• pint-stable: display fixpoints just in time

Changes:

• Dropped pint-nusmv and pint-its (moved to pypint)

Pint 2018-07-10

New features:

• pint-export: PNML format

Improvements:

• model reduction has been refactored to offer stable performance

Pint 2018-03-22

Bugfix:

• support empty models as input

Pint 2017-12-19

Minor changes

• PINT_SHARE_PATH environment variable always has priority
• pint-export -l nusmv: add supports for --mapfile and --no-init option

Pint 2017-09-25

New features

• support for simultaneous transitions in pint-reach, pint-stable, pint-lcg, pint-its, pint-nusmv, pint-mole

Pint 2017-04-13

NEW: Python interface

• pypint module
• customization of Jupyter notebook web interface

New features

• pint-reach: support for or in goal specification
• pint-reach: add --oneshot-mutations-for-cut option for computing initial state mutations preventing the given goal
• pint-export: add --lock option
• pint-export --squeeze: add support for --squeeze-preserve option
• most of commands have a --json-stdout argument for making output programmatically exploitable.

New commands

• pint_install_deps: install runtime dependencies for Pint.

Pint 2016-12-15

New features:

• pint-reach --bifurcations --bifurcations-mode mole+ua: use mole to compute the set of reachable states prior to identifying bifurcation transitions.
• Preliminary support of simultaneous transitions of the form

{a 0 -> 1; b 0 -> 1} when c=1

In this example, when a=0,b=0,c=1, the transition will change simultaneously a and b.
This is fully supported by pint-sg command ; others will throw an exception as it is not supported yet.

Improvements:

• pint-export --simplify: use Quine-McCluskey algorithm to improve transitions simplification

Pint 2016-09-16

New features:

• pint-reach --bifurcations: identifies bifurcation transitions for goal (under-approximation)

Bugfixes:

• fix NuSMV export with non-deterministic automata (affects pint-nusmv and pint-export)

Pint 2016-05-09

New tools:

• pint-nusmv: model-checking with NUSMV

New features:

• pint-sg: add --state-graph option to export reachable state graph
• pint-reach: add --no-init-cutsets to ignore cut sets with local states in the initial state
• pint-reach: new implementation of under-approximation with ASP (requires clingo), old can still be used with --legacy option, but will be removed in a few months.