Realizability (kind2dev@731decdf5fb1.Realizability)

type 'a analyze_func =
  bool ->
  Lib.kind_module list ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  unit

type unrealizable_result

type realizability_result =

| Realizable of Term.t
| Unrealizable of unrealizable_result
| Unknown

Result of a realizability check

val result_to_string : realizability_result -> string

val function_certificate : 
  unrealizable_result ->
  (int * (StateVar.t * Model.value list) list) list option

The input traces of a function, with their lengths, on which no function satisfies its contract, if the contract was proven unrealizable by FunctionRealizability, or None

val unrealizable_function : 
  (int * (StateVar.t * Model.value list) list) list ->
  realizability_result

The result for the input traces of a function on which no function satisfies its contract

val realizability_check : 
  ?include_invariants:bool ->
  (Term.t -> Var.VarSet.t) ->
  TransSys.t ->
  Var.t list ->
  Var.t list ->
  Var.t list ->
  realizability_result

Checks whether there exists an implementation that satisfies a given specification

realizability_check m s c0 v1 c1 checks whether the specification represented by transition system s is realizable or not under the assumption that c0 is the list of controllable variables at offset 0, v1 is the list of variables at offset 1, c1 is the list of variables at offset 1, and all terms in s without controllable variables are assumed to hold. It uses function m to get the set of variables of a term.

exception Trace_or_conflict_computation_failed of string

val compute_deadlocking_trace_and_conflict : 
  'a analyze_func ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  Var.t list ->
  Var.t list ->
  unrealizable_result ->
  (StateVar.t * Model.value list) list * ModelElement.loc_core