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.

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



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