module Bwd:`sig`

..`end`

Backward reachability with approximation

This algorithm of backward reachability performs approxmations guided by an
oracle. It is parameterized by a structure of priority queue to define a
search strategy.

Backward reachability with approximation

This algorithm of backward reachability performs approxmations guided by an
oracle. It is parameterized by a structure of priority queue to define a
search strategy.

module type PriorityNodeQueue =`sig`

..`end`

`type `

result =

`|` |
`Safe of ` |
`(*` | The system is safe and we return the set of visited nodes and the inferred invariants | `*)` |

`|` |
`Unsafe of ` |
`(*` | The system is unsafe and we return the faulty node and the full list of candidate invariants that were considered | `*)` |

module type Strategy =`sig`

..`end`

module Make:

Functor for creating a strategy given a priority queue

module BFS:`Strategy`

module DFS:`Strategy`

module BFSH:`Strategy`

module DFSH:`Strategy`

module BFSA:`Strategy`

module DFSA:`Strategy`

module Selected:`Strategy`

Strategy selected by the options of the command line