Rtm_AllocateRegionStruct()
required
Rtm_AssignmentsBuildMdd()
builds the mdd for the assignments of a command
Rtm_AtomBuildInitCmdListMdds()
updates mdds by processing the init commands of the atom
Rtm_AtomBuildInitialRegion()
build initial region for an atom in a timed module
Rtm_AtomBuildTransitionRelation()
build transition relation for an atom
Rtm_AtomBuildUpdateCmdListMdds()
updates mdds by processing the update commands of the atom
Rtm_AtomBuildWaitCmdListMdds()
updates mdds by processing the wait(delay) commands of the atom
Rtm_AtomProcessDefaultInitCommand()
updates mdds by processing the default init command of the atom
Rtm_AtomProcessDefaultUpdateCommand()
updates mdds by processing the default update command of the atom
Rtm_AtomProcessImplicitUpdateCommand()
Process the implicit command for the update command list of an atom
Rtm_BuildOneWaitAssignmentMdd()
builds the mdd for a single assignment of a wait command
Rtm_BuildUnconstrainedTimerIncMdd()
Builds the mdd for timers not constrained by a wait command
Rtm_DebugTracePrint()
print debug trace for an invariant for timed modules
Rtm_End()
Closes the rtm package
Rtm_GuardBuildMdd()
builds the mdd for the guard of a command
Rtm_InitAssignmentsBuildMdd()
builds the mdd for the assignments of an init command
Rtm_Init()
Initializes the rtm package
Rtm_MddPickMinterm()
required
Rtm_MddPrintCubes()
required
Rtm_ModuleBuildInitialRegion()
build mdd for initial region of module
Rtm_ModuleBuildTransitionRelation()
build transition relation (as an MDD) for a timed module
Rtm_ModulePerformBFS()
do invariant checking on a timed module
Rtm_RegionManagerAddModuleToRtmInfo()
required
Rtm_RegionManagerAlloc()
required
Rtm_RegionManagerObtainRtmInfoFromModule()
required
Rtm_RegionManagerReadRegionTable()
required
Rtm_Reinit()
Re-initializes the rtm package
Rtm_RtmRegionManagerIncrementCounter()
required
Rtm_RtmRegionManagerReadCounter()
required
Rtm_WaitAssignmentsBuildMdd()
builds the mdd for all of the assignments of a wait command

Last updated on 980624 22h11