Module dev.civl.mc

Package dev.civl.mc.kripke.IF

Interface LibraryEnabler

public interface LibraryEnabler

A Library Enabler provides a method to compute the enabled transitions of system function calls at a certain state for a give process. It also provides a method to compute the ample set of processes at a given state for a given process. A new library is implemented in the package named as "dev.civl.mc.library." ( CIVLConstants.LIBRARY_PREFIX) + library name. And the class name of the enabler is: "Lib" + library name + "Enabler". For example, the stdio library enabler is implemented as the class dev.civl.mc.library.stdio.LibstdioEnabler.

Method Summary

Modifier and Type	Method	Description
BitSet	ampleSet(State state, int pid, CallOrSpawnStatement statement, MemoryUnitSet[] setsReachableRead, MemoryUnitSet[] setsReachableWrite)	Computes the ample set process IDs from a system function call at a given state for a given process.
List<Transition>	enabledTransitions(State state, CallOrSpawnStatement call, dev.civl.sarl.IF.expr.BooleanExpression pathCondition, int pid)	Computes the enabled transitions of a given function call.

Method Details

ampleSet

BitSet ampleSet(State state,
 int pid,
 CallOrSpawnStatement statement,
 MemoryUnitSet[] setsReachableRead,
 MemoryUnitSet[] setsReachableWrite)
         throws UnsatisfiablePathConditionException

Computes the ample set process IDs from a system function call at a given state for a given process.

Precondition: the call statement is enabled at the given state and it is one of the outgoing statements of process pid.

Contract: nothing dependent on the given statement can occur without one of the transitions of the processes in the returned ample set occurring first.

Parameters:

state - The current state.

pid - The ID of the process that the system function call belongs to.

statement - The system function call statement.

reachablePtrWritableMap -

reachablePtrReadonlyMap -

reachableNonPtrWritableMap -

reachableNonPtrReadonlyMap -

reachableMemUnitsMap - The map of reachable memory units of all active processes.

Returns:

the ample set of process IDs

Throws:

UnsatisfiablePathConditionException

enabledTransitions

List<Transition> enabledTransitions(State state,
 CallOrSpawnStatement call,
 dev.civl.sarl.IF.expr.BooleanExpression pathCondition,
 int pid)
                             throws UnsatisfiablePathConditionException

Computes the enabled transitions of a given function call. This is to support nondeterministic function calls.

Parameters:

state - The current state.

call - The function call statement, upon which the set of enabled transitions will be computed.

pathCondition - The current path condition.

pid - The ID of the process that the function call belongs to.

Returns:

The set of enabled transitions.

Throws:

UnsatisfiablePathConditionException