Module Validator


module Validator: sig .. end
Inductive invariant checking and path feasibility.

This module provides simple functions to validate the results returned by model-checkers. The implementation of this module is intentionally separated from that of model-checkers. The goal here is to provide functions that are simple and (hopefully) easy to read, with little regard for efficiency.


module Make: 
functor (A : Model.S) -> sig .. end
Functor providing inductive invariant checking and path feasibility checking functions for a given model.