Trait

analyzers

SafetyTheory

Related Doc: package analyzers

Permalink

trait SafetyTheory extends AnyRef

Created by kdelmas on 25/09/17.

Self Type
SafetyTheory with Parsing with SMTTranslation with STMDDBuilder
Linear Supertypes
AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SafetyTheory
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class Choose(subVar: SubstitutionVar, value: Int) extends (SafetyTheory.this)#ModelPredicate with Product with Serializable

    Permalink

    Case class encoding the choice over a substitution varaible

    Case class encoding the choice over a substitution varaible

    subVar

    the substitution variable

    value

    the value of the variable

  2. type Clause = Seq[(SafetyTheory.this)#ModelPredicate]

    Permalink

    type representing a clause as a set of predicate

  3. type Model = Seq[(SubstitutionVar, Int)]

    Permalink

    type representing a model as a mapping of substitution variable to an integer encoding the selected substitution

  4. sealed trait ModelPredicate extends (SafetyTheory.this)#SafetyPredicate

    Permalink

    Base trait for model predicates

  5. case class Neg(p: (SafetyTheory.this)#Choose) extends (SafetyTheory.this)#ModelPredicate with Product with Serializable

    Permalink

    Util case class for negation of Safety predicates

    Util case class for negation of Safety predicates

    p

    the safety predicate to negate

  6. case class SafeOrder(stmdd: ((SafetyTheory.this)#mddFactory)#MDD, req: Int) extends (SafetyTheory.this)#SafetyReqPredicate with Product with Serializable

    Permalink

    Case class encoding the order requirement predicate

    Case class encoding the order requirement predicate

    stmdd

    the STMDD representing the system

    req

    the order requirement

  7. case class SafeR(stmdd: ((SafetyTheory.this)#mddFactory)#MDD, req: Real) extends (SafetyTheory.this)#SafetyReqPredicate with Product with Serializable

    Permalink

    Case class encoding the reliability requirement predicate

    Case class encoding the reliability requirement predicate

    stmdd

    the STMDD representing the system

    req

    the reliability requirement

  8. sealed trait SafetyPredicate extends AnyRef

    Permalink

    Base trait for safety theory predicates

  9. sealed trait SafetyReqPredicate extends (SafetyTheory.this)#SafetyPredicate

    Permalink

    Base trait for requirement predicates

  10. type SelectionSeq = Seq[(PathIdentType, Option[Int])]

    Permalink

    type representing a mapping of component instance identifier to optional integer encoding the selected substitution

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  5. def checkSat(cube: Seq[(SafetyTheory.this)#SafetyPredicate], withXplain: Boolean = true): Either[(SafetyTheory.this)#Model, (SafetyTheory.this)#Clause]

    Permalink

    Decision procedure of the Safety theory

    Decision procedure of the Safety theory

    cube

    the conjonction of Safety predicate on which the satisfiability modulo Safety must be decided

    withXplain

    use quickXplain conflict clause minimisation

    returns

    a model if SAT or a conflict clause if UNSAT

  6. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  7. val computeUnr: ((((SafetyTheory.this)#mddFactory)#MDD, (SafetyTheory.this)#SelectionSeq)) ⇒ ProbMeasure

    Permalink

    Memoized computation of the unreliability of an STMDD according to a selection

  8. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. def getChoiceIndex(choice: (SafetyTheory.this)#SelectionSeq, of: ((SafetyTheory.this)#mddFactory)#MDDNode): Int

    Permalink
  12. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  13. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  14. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  15. def modelToSelectionSeq(stmdd: ((SafetyTheory.this)#mddFactory)#MDD, m: (SafetyTheory.this)#Model): (SafetyTheory.this)#SelectionSeq

    Permalink

    Transform a model of the substitution variables to a list of selection index in the local indicators table of the STMDD edges

    Transform a model of the substitution variables to a list of selection index in the local indicators table of the STMDD edges

    stmdd

    the STMDD concerned by the model

    m

    the model of the substitution variables

    returns

    the selection sequence

  16. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  17. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  18. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  19. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  20. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  21. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  23. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped