imcCmd.c

Command interface for the imc package.

By: Jae-Young Jang

Imc_Init(): Initializes the imc package.
Imc_End(): Ends the imc package.
CommandImc(): The iterative_model_check command.
IterativeModelCheckUsage(): Prints the usage of the iterative_model_checking command.
TimeOutHandle(): Handle the timeout signal.

imcImc.c

Incremental Model Checker.

By: Jae-Young Jang

Imc_ImcEvaluateFormulaLinearRefine(): Verify a formula with incremental refinement.
Imc_ImcVerifyFormula(): Verify a formula.
Imc_SatCheck(): Check if a formula is true or false.
Imc_ImcInfoInitialize(): Initializes an imcInfo structure for the given method.
Imc_ImcInfoFree(): Free an imcInfo structure for the given method.
Imc_SystemInfoInitialize(): Initilalize a system info.
Imc_SystemInfoFree(): Free a system info.
Imc_ImcSystemInfoUpdate(): Update a system info.
Imc_UpperSystemInfoInitialize(): Initilalize an upper-bound approximate system info.
Imc_UpperSystemMinimize(): Minimize the size of a upper-bound transition relation.
Imc_UpperSystemInfoFree(): Free a upper-bound approximate system info.
Imc_LowerSystemInfoInitialize(): Initilalize a lower-bound approximate system info.
Imc_LowerSystemMinimize(): Minimize the size of a lower-bound transition relation.
Imc_LowerSystemInfoFree(): Free a lower-bound approximate system info.
Imc_NodeInfoInitialize(): Initilalize node info.
Imc_NodeInfoReset(): Reset node info.
Imc_NodeInfoFree(): Free node info.
Imc_ImcPrintSystemSize(): Print global system size.
Imc_ImcPrintApproxSystemSize(): Print upper-system size.
Imc_GetUpperSat(): Get a upperbound satisfying states of a given formula.
Imc_GetLowerSat(): Get a lowerbound satisfying states of a given formula.
Imc_ImcEvaluateCTLFormula(): Model check formula with approxmiations.
Imc_ImcEvaluateEXApprox(): Evaluate EX formula with approximations.
Imc_ImcEvaluateEUApprox(): Evaluate EU formula with approximations.
Imc_ImcEvaluateEGApprox(): Evaluate EG formula with approximations.
Imc_ComputeUpperPreimage(): Compte a supperset of exact pre image.
Imc_ComputeApproxPreimageByQuantification(): Compte a superset or a subset of exact pre image.
Imc_ComputeLowerPreimage(): Compte a subset of exact pre image.
Imc_ComputeLowerPreimageBySubsetTR(): Compte a subset of exact pre image by subsetting some transition sub-relations.
Imc_ProductAbstract(): Compute a product of relation array. All variables in smoothVarsMddIdArray are quntified during product.
ImcCreateScheduleArray(): Create an refinement schedule array.
ImcModelCheckAtomicFormula(): Find Mdd for states satisfying Atomic Formula.
ImcModelCheckTrueFalseFormula(): Compute TRUE or FALSE expression.
ImcModelCheckNotFormula(): Compute NOT expression.
ImcModelCheckAndFormula(): Compute AND expression.
ImcPrintLatchInApproxSystem(): Print latch names in an upper approximate system.
ImcNodeInfoTableFree(): Free node info table.
stringCompare(): Compare two strings

Last updated on 20010517 18h00

Contact