case class State(procs: Procs, store: Store[Addr, Abs], kstore: KontStore[KontAddr]) extends Product with Serializable
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- State
- Serializable
- Serializable
- Product
- Equals
- AnyRef
- Any
Implicitly
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
Visibility
- 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
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate() @throws( ... )
- 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
- def hasError: Boolean
- def integrate(p: PID, ctx: Context, act: ActionHelpers.Act): Set[(State, PID, Option[ActorEffect])]
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val kstore: KontStore[KontAddr]
- def macrostepAll(sem: Semantics[Exp, Abs, Addr, Time]): Set[(Set[(State, Option[ActorEffect])], PID, G)]
-
def
macrostepPid(p: PID, sem: Semantics[Exp, Abs, Addr, Time]): Option[(G, Set[(State, Option[ActorEffect])])]
Performs a macrostep for a given PID.
Performs a macrostep for a given PID. If the state is stuck, returns None. Otherwise, returns the graph explored for this macrostep, as well as every final state and the effect that stopped the macrostep for that state. The final states *are* in the graph (unlike macrostepTrace), because we need to keep track of the edge.
-
def
macrostepPidTrace(p: PID, sem: Semantics[Exp, Abs, Addr, Time]): Option[(State, List[State])]
Performs a macrostep for a given PID, restricted only to macrosteps that produce linear traces.
Performs a macrostep for a given PID, restricted only to macrosteps that produce linear traces. If the state is stuck, returns None. Otherwise, returns the final state of the macrostep, as well as the trace explored to reach that state (not including the final state).
- def macrostepTraceAll(sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, List[State])]
- def macrostepTraceAny(sem: Semantics[Exp, Abs, Addr, Time]): Option[(State, PID, List[State])]
-
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()
- val procs: Procs
- def stepAll(sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, Option[ActorEffect])]
- def stepAllExceptPid(p: PID, sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, Option[ActorEffect])]
- def stepAny(sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, Option[ActorEffect])]
- def stepPid(p: PID, sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, Option[ActorEffect])]
- def stepPids(pids: Set[PID], sem: Semantics[Exp, Abs, Addr, Time]): Set[(State, PID, Option[ActorEffect])]
- val store: Store[Addr, Abs]
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- def toXml: List[Node]
-
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)