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	`*)`

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