Module Bwd (.ml)

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 Node.t list * Node.t list (*The system is safe and we return the set of visited nodes and the inferred invariants*)
| Unsafe of Node.t * Node.t list (*The system is unsafe and we return the faulty node and the full list of candidate invariants that were considered*)

Strategies


module type Strategy = sig .. end
module Make: 
functor (Q : PriorityNodeQueue) -> Strategy
Functor for creating a strategy given a priority queue

Predefined Strategies


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