Module Aorai_option

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