val debug_each : string -> unittype resource = | Process| Function| Semaphore| Event| Logbook| SamplingPort| QueuingPort| Buffer| Blackboard
type partition_mode = | Idle| Cold_Start| Warm_Start| Normal
val min_partition_mode : intval max_partition_mode : inttype queuing_discipline = | Fifo| Prio
val min_queuing_discipline : intval max_queuing_discipline : intval string_of_queuing_discipline : int64 -> stringtype return_code = | NO_ERROR| NO_ACTION| NOT_AVAILABLE| INVALID_PARAM| INVALID_CONFIG| INVALID_MODE| TIMED_OUT
val min_return_code : intval max_return_code : intval pname_ErrorHandler : stringtype action = | Nop| Cond of string * string| Assign of string * string| Call of string| LockPreemption| UnlockPreemption| SetPartitionMode of partition_mode option| CreateProcess of Action.process| CreateErrorHandler of id * CilType.Varinfo.t| Start of id| Stop of id| Suspend of id| SuspendSelf of id * time| Resume of id| CreateBlackboard of id| DisplayBlackboard of id| ReadBlackboard of id * time| ClearBlackboard of id| CreateSemaphore of Action.semaphore| WaitSemaphore of id * time| SignalSemaphore of id| CreateEvent of id| WaitEvent of id * time| SetEvent of id| ResetEvent of id| TimedWait of time| PeriodicWait
val action_of_edge : ('a * 'b * 'c * 'd) -> 'bval get_a : ('a * 'b * 'c * 'd) -> 'aval get_b : ('a * 'b * 'c * 'd) -> 'dval add_edge : id -> edge -> unitval filter_map_actions : (action -> 'a option) -> 'a listval funs_for_process : id -> Cil.varinfo listmodule type GenSig = sig ... endval add_return_var : id -> [ `Read | `Write ] -> string -> unitval is_global : string -> boolval get_locals : id -> string listval get_globals : unit -> string listval str_resource : id -> stringval str_resources : id list -> stringval str_return_code : string option -> stringval id_pml : (resource * string) -> int64val str_id_pml : (resource * string) -> stringval str_pid_pml : (resource * string) -> stringval str_ids_pml : (resource * string) list -> (string -> string) -> stringval action_may_fail : action -> boolval str_action_pml : id -> string option -> action -> stringval find_option : ('a -> bool) -> 'a list -> 'a optionval simplify : unit -> unitval validate : unit -> unitval print_actions : unit -> unitval save_result : string -> string -> string -> unitval save_dot_graph : unit -> unitval save_promela_model : unit -> unit