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 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