Module Aorai_option

module Aorai_option: sig .. end

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.