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.