Module Validator
module Validator:Inductive invariant checking and path feasibility.sig
..end
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 providing inductive invariant checking and path feasibility checking
functions for a given model.