ContractChecker (kind2dev@731decdf5fb1.ContractChecker)

val check_contract_realizability : 
  'a InputSystem.t ->
  TransSys.t ->
  Realizability.realizability_result

Checks whether there exists an implementation that satisfies a given specification

check_contract_realizability i s checks whether the contract represented by transition system s is realizable or not. It assumes s was generated from the contract of the subsystem in i which has the same scope than s.

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

val pp_print_realizability_result_pt : 
  'a Realizability.analyze_func ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  Stdlib.Format.formatter ->
  Realizability.realizability_result ->
  unit

val pp_print_realizability_result_json : 
  'a Realizability.analyze_func ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  Stdlib.Format.formatter ->
  Realizability.realizability_result ->
  unit

val pp_print_realizability_result_xml : 
  'a Realizability.analyze_func ->
  'a InputSystem.t ->
  Analysis.param ->
  TransSys.t ->
  Stdlib.Format.formatter ->
  Realizability.realizability_result ->
  unit

type satisfiability_result =

| Satisfiable
| Unsatisfiable
| Unknown

Result of a satisfiability check

val satisfiability_result_to_string : satisfiability_result -> string

val check_contract_satisfiability : TransSys.t -> satisfiability_result

Checks whether a given specification is satisfiable

check_contract_satisfiability i s checks whether the contract represented by transition system s is satisfiable or not.

val pp_print_satisfiability_result_pt : 
  'a InputSystem.t ->
  Analysis.param ->
  Stdlib.Format.formatter ->
  satisfiability_result ->
  unit

val pp_print_satisfiability_result_json : 
  Stdlib.Format.formatter ->
  satisfiability_result ->
  unit

val pp_print_satisfiability_result_xml : 
  Stdlib.Format.formatter ->
  satisfiability_result ->
  unit