case class State(control: AAMNS.Control, store: Store[Addr, Abs], kstore: KontStore[KontAddr], a: KontAddr, t: Time) extends Product with Serializable
A machine state is made of a control component, a value store, a continuation store, and an address representing where the current continuation lives.
- Alphabetic
- By Inheritance
- State
- Serializable
- Serializable
- Product
- Equals
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- All
Instance Constructors
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (State, B)
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val a: KontAddr
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate() @throws( ... )
- val control: AAMNS.Control
- def ensuring(cond: (State) ⇒ Boolean, msg: ⇒ Any): State
- def ensuring(cond: (State) ⇒ Boolean): State
- def ensuring(cond: Boolean, msg: ⇒ Any): State
- def ensuring(cond: Boolean): State
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def formatted(fmtstr: String): String
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
def
halted: Boolean
Checks if the current state is a final state.
Checks if the current state is a final state. It is the case if it reached the end of the computation, or an error
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val kstore: KontStore[KontAddr]
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
def
step(sem: Semantics[Exp, Abs, Addr, Time]): Set[State]
Computes the set of states that follow the current state
- def stepAnalysis[L](analysis: Analysis[L, Exp, Abs, Addr, Time], current: L): L
- val store: Store[Addr, Abs]
-
def
subsumes(that: State): Boolean
Checks whether a states subsumes another, i.e., if it is "bigger".
Checks whether a states subsumes another, i.e., if it is "bigger". This is used to perform subsumption checking when exploring the state space, in order to avoid exploring states for which another state that subsumes them has already been explored.
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- val t: Time
-
def
toString(): String
- Definition Classes
- State → AnyRef → Any
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
- def →[B](y: B): (State, B)