module Aorai_option: sig
.. end
true
if the user declares that its ya automaton is deterministic.
include Plugin.S
module Ltl_File: Parameter_sig.String
module To_Buchi: Parameter_sig.String
module Buchi: Parameter_sig.String
module Ya: Parameter_sig.String
module Output_Spec: Parameter_sig.Bool
module Output_C_File: Parameter_sig.String
module Dot: Parameter_sig.Bool
module DotSeparatedLabels: Parameter_sig.Bool
module AbstractInterpretation: Parameter_sig.Bool
module Axiomatization: Parameter_sig.Bool
module ConsiderAcceptance: Parameter_sig.Bool
module AutomataSimplification: Parameter_sig.Bool
module Test: Parameter_sig.Int
module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
module Deterministic: State_builder.Ref
with type data = bool
true
if the user declares that its ya automaton is deterministic.
val is_on : unit -> bool
val promela_file : unit -> string
val advance_abstract_interpretation : unit -> bool
val emitter : Emitter.t
The emitter which emits Aorai annotations.
Since Oxygen-20120901