Packages

c

ConcurrentAAM

class ConcurrentAAM[Exp, Abs, Addr, Time, TID] extends AbstractMachine[Exp, Abs, Addr, Time]

Linear Supertypes
AbstractMachine[Exp, Abs, Addr, Time], AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ConcurrentAAM
  2. AbstractMachine
  3. AnyRef
  4. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new ConcurrentAAM(exploration: ExplorationType)(implicit arg0: Expression[Exp], arg1: JoinLattice[Abs], arg2: Address[Addr], arg3: Timestamp[Time], arg4: ThreadIdentifier[TID])

Type Members

  1. trait Output extends AnyRef

    The output of the abstract machine

    The output of the abstract machine

    Definition Classes
    AbstractMachine
  2. type Annot = (TID, Effects)
  3. case class ConcurrentAAMOutput(halted: Set[State], numberOfStates: Int, time: Double, graph: Option[G], timedOut: Boolean) extends Output with Product with Serializable
  4. case class Context(control: AAM.Control, kstore: KontStore[KontAddr], a: KontAddr, t: Time) extends Product with Serializable
  5. type Effects = Set[Effect[Addr]]
  6. type Exploration = (State, Set[State]) ⇒ Set[(TID, Effects, State)]
  7. type G = Graph[State, Annot, Unit]
  8. type KontAddr = AAM.KontAddr
  9. case class State(threads: ThreadMap, results: ThreadResults, store: Store[Addr, Abs]) extends Product with Serializable
  10. case class ThreadMap(content: Map[TID, Set[Context]]) extends Product with Serializable
  11. case class ThreadResults(content: Map[TID, Abs]) extends Product with Serializable

Value Members

  1. val aam: AAM[Exp, Abs, Addr, Time]
  2. def abs: JoinLattice[Abs]
  3. def addr: Address[Addr]
  4. implicit val annot: GraphAnnotation[Annot, Unit]
  5. def effectsToStr(effs: Effects): String
  6. def eval(exp: Exp, sem: Semantics[Exp, Abs, Addr, Time], graph: Boolean, timeout: Timeout): Output

    Evaluates a program, given a semantics.

    Evaluates a program, given a semantics. If @param graph is true, the state graph will be computed and stored in the output. Returns an object implementing the Output trait, containing information about the evaluation. @param timeout is the timeout in ns, when reached, the evaluation stops and the currently computed results are returned.

    Definition Classes
    ConcurrentAAM → AbstractMachine
  7. def exp: Expression[Exp]
  8. implicit val graphNode: GraphNode[State, Unit]
  9. def name: String

    The name of the abstract machine

    The name of the abstract machine

    Definition Classes
    ConcurrentAAM → AbstractMachine
  10. val noEffect: Effects
  11. def thread: ThreadIdentifier[TID]
  12. def time: Timestamp[Time]
  13. object CannotHandle extends Exception with Product with Serializable
  14. object State extends Serializable
  15. object ThreadMap extends Serializable