Module dev.civl.mc
Package dev.civl.mc.state.IF
package dev.civl.mc.state.IF
Module state is responsible for the creation and manipulation of
states of a CIVL model.
The entry point to this module in the class
States.
This class provides static method to obtain state factories. The state factory
is used to produce new states and modify states.
The interface for this module is provided in package dev.civl.mc.state.IF.
That package defines interfaces for the state factory, the state itself,
and various sub-components of the state. Users of this module should
use only elements from the interface, not the implementation packages.
There are currently two alternative implementations of the state module:
immutable and transient. In the immutable implementation, states
and their components are (essentially) immutable. In the transient
module states (and their components) begin in a mutable state but
can be made immutable at any time by invoking a "commit" method.
The relative advantages and disadvantages of the two approaches are
being explored.-
ClassDescriptionExtends an execution exception with a state at which error occurred.Extends an execution exception with a state at which error occurred.A DynamicScope is a runtime instance of a static scope.A memory unit represents an object or a part of an object that can be accessed through an expression, e.g., a[9].x, b[8], c, etc.A memory unit set represents a set of memory units.A ProcessState represents the state of a process (thread of execution) in a CIVL model.An entry on a call stack of a process; also known as an "activation frame".A State represents the (global) state of a CIVL Model.The state factory is used to create all state objects.Entry point for the state module: provides a static method to get a new state factory.Thrown when a path condition becomes unsatisfiable, typically due to a side effect from evaluating an expression.