Trait

analyzers

DSEProblemSolverAll

Related Doc: package analyzers

Permalink

trait DSEProblemSolverAll extends DSEProblemSolverKCRSim with DSEProblemSolverHipHOPS

Trait containing DSE problem resolution with HIPHOPS and SMT

Self Type
DSEProblemSolverAll with Parsing with SMTTranslation with SubstitutionAnalyzerSim with STMDDBuilderSim with TraceInterpreter
Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DSEProblemSolverAll
  2. DSEProblemSolverHipHOPS
  3. DSEProblemSolverKCRSim
  4. SafetyTheory
  5. DSEProblemSolverKCR
  6. DSEProblemSolver
  7. ConfigurationAnalyzer
  8. Analyser
  9. AnyRef
  10. 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

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

    Permalink

    type representing a clause as a set of predicate

    type representing a clause as a set of predicate

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

    Permalink

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

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

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

    Permalink

    Base trait for model predicates

    Base trait for model predicates

    Definition Classes
    SafetyTheory
  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

    Definition Classes
    SafetyTheory
  6. class OrderedCompInstIdent extends Ordered[(ConfigurationAnalyzer.this)#OrderedCompInstIdent]

    Permalink

    Class encoding instance identifiers which can be ordered

    Class encoding instance identifiers which can be ordered

    Definition Classes
    ConfigurationAnalyzer
  7. class OrderedCompTrace extends Ordered[(ConfigurationAnalyzer.this)#OrderedCompTrace]

    Permalink

    Class encoding of component traces which can be ordered

    Class encoding of component traces which can be ordered

    Definition Classes
    ConfigurationAnalyzer
  8. class OrderedSymbol extends Ordered[(ConfigurationAnalyzer.this)#OrderedSymbol]

    Permalink

    Class encoding scala Symbol that can be compared

    Class encoding scala Symbol that can be compared

    Definition Classes
    ConfigurationAnalyzer
  9. 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

    Definition Classes
    SafetyTheory
  10. 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

    Definition Classes
    SafetyTheory
  11. sealed trait SafetyPredicate extends AnyRef

    Permalink

    Base trait for safety theory predicates

    Base trait for safety theory predicates

    Definition Classes
    SafetyTheory
  12. sealed trait SafetyReqPredicate extends (SafetyTheory.this)#SafetyPredicate

    Permalink

    Base trait for requirement predicates

    Base trait for requirement predicates

    Definition Classes
    SafetyTheory
  13. type SelectionSeq = Seq[(PathIdentType, Option[Int])]

    Permalink

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

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

    Definition Classes
    SafetyTheory
  14. type Solution = Map[CompInstanceIdent, CompAlternative]

    Permalink

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. object OrderedCompInstIdent

    Permalink

    Companion object for ordered instance identifiers

    Companion object for ordered instance identifiers

    Definition Classes
    ConfigurationAnalyzer
  5. object OrderedCompTrace

    Permalink

    Companion object of component traces

    Companion object of component traces

    Definition Classes
    ConfigurationAnalyzer
  6. object OrderedSymbol

    Permalink

    Companion object for ordered symbols

    Companion object for ordered symbols

    Definition Classes
    ConfigurationAnalyzer
  7. object Solver

    Permalink

    Solver object handling classic Z3 Boolean assertions and custom Safety assertions

    Solver object handling classic Z3 Boolean assertions and custom Safety assertions

    Definition Classes
    DSEProblemSolverKCR
  8. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  9. def checkSat(cube: Seq[(DSEProblemSolverAll.this)#SafetyPredicate], withXplain: Boolean = true): Either[(DSEProblemSolverAll.this)#Model, (DSEProblemSolverAll.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

    Definition Classes
    SafetyTheory
  10. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  11. implicit object compBasicFlow extends Ordering[BasicFlowIdent]

    Permalink

    Order over flow identifiers

    Order over flow identifiers

    Definition Classes
    ConfigurationAnalyzer
  12. implicit object compFlowConst extends Ordering[FlowConst]

    Permalink

    Order over constants

    Order over constants

    Definition Classes
    ConfigurationAnalyzer
  13. implicit object compOrder extends Ordering[CompInstanceIdent]

    Permalink

    Order over instance identifiers in a system component

    Order over instance identifiers in a system component

    Definition Classes
    ConfigurationAnalyzer
  14. val computeUnr: ((((DSEProblemSolverAll.this)#mddFactory)#MDD, (DSEProblemSolverAll.this)#SelectionSeq)) ⇒ ProbMeasure

    Permalink

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

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

    Definition Classes
    SafetyTheory
  15. val designSpaceExplorationHipHopProfiler: Profiler[Unit, Option[(DSEProblemSolverAll.this)#Solution]]

    Permalink
    Definition Classes
    DSEProblemSolverHipHOPS
  16. val designSpaceExplorationProfiler: Profiler[DesignSpaceExplorationMethod, Option[(DSEProblemSolverAll.this)#Solution]]

    Permalink
  17. val designSpaceExplorationProfilerKCR: Profiler[Unit, Option[(DSEProblemSolverAll.this)#Solution]]

    Permalink

    Timed DSE resolution

    Timed DSE resolution

    Definition Classes
    DSEProblemSolverKCR
  18. final def eq(arg0: AnyRef): Boolean

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

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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  21. def generateDecisionVars(): List[SubstitutionVar]

    Permalink

    Generate substitution variables for component instance in the system

    Generate substitution variables for component instance in the system

    returns

    list of substitution var

    Definition Classes
    DSEProblemSolverKCRSimDSEProblemSolver
  22. def getChoiceIndex(choice: (DSEProblemSolverAll.this)#SelectionSeq, of: ((DSEProblemSolverAll.this)#mddFactory)#MDDNode): Int

    Permalink
    Definition Classes
    SafetyTheory
  23. final def getClass(): Class[_]

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

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

    Permalink
    Definition Classes
    Any
  26. def modelToSelectionSeq(stmdd: ((DSEProblemSolverAll.this)#mddFactory)#MDD, m: (DSEProblemSolverAll.this)#Model): (DSEProblemSolverAll.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

    Definition Classes
    SafetyTheory
  27. final def ne(arg0: AnyRef): Boolean

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

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

    Permalink
    Definition Classes
    AnyRef
  30. lazy val solution: Option[(DSEProblemSolverAll.this)#Solution]

    Permalink

    solution of the DSE problem

    solution of the DSE problem

    Definition Classes
    DSEProblemSolverKCRDSEProblemSolver
  31. def solveConf(withXplain: Boolean = true): Option[(DSEProblemSolverAll.this)#Solution]

    Permalink

    Solve the DSE problem of the actual configuration conf

    Solve the DSE problem of the actual configuration conf

    withXplain

    use quickXlain conflict clause minimisation algorithm

    returns

    solution if it exists

    Definition Classes
    DSEProblemSolverKCR
  32. def solveConfWithReq(RObj: Option[Real], cardObj: Option[Int], withXplain: Boolean = true): Option[(DSEProblemSolverAll.this)#Solution]

    Permalink

    Solve the DSE problem using custom reliability and order requirements

    Solve the DSE problem using custom reliability and order requirements

    RObj

    optional reliability requirement

    cardObj

    optional order requirement

    withXplain

    use quickXlain conflict clause minimisation algorithm

    returns

    solution if it exists

    Definition Classes
    DSEProblemSolverKCR
  33. def solveWith(method: DesignSpaceExplorationMethod, rReq: Option[Real] = None, cReq: Option[Int] = None): Option[(DSEProblemSolverAll.this)#Solution]

    Permalink

    Solve DSE method with custom requirements and a given method

    Solve DSE method with custom requirements and a given method

    method

    resolution method

    rReq

    optionnal reliability requirement

    cReq

    optionnal order requirement

    returns

    solution if any

  34. def solveWithHipHOP(reliabilityReq: Option[String] = None): Option[(DSEProblemSolverAll.this)#Solution]

    Permalink

    Solve DSE problem using HIPHOPS

    Solve DSE problem using HIPHOPS

    reliabilityReq

    reliability requirement if defined, otherwise optimised

    returns

    Solution if at least one found by HIPHOPS

    Definition Classes
    DSEProblemSolverHipHOPS
  35. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  36. implicit def toOSymb(s: Symbol): (DSEProblemSolverAll.this)#OrderedSymbol

    Permalink

    implicit transformation from Symbol to Ordered Symbol

    implicit transformation from Symbol to Ordered Symbol

    s

    Scala Symbol

    returns

    ordered symbol

    Definition Classes
    ConfigurationAnalyzer
  37. def toString(): String

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

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

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

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

Inherited from DSEProblemSolverHipHOPS

Inherited from DSEProblemSolverKCRSim

Inherited from SafetyTheory

Inherited from DSEProblemSolverKCR

Inherited from DSEProblemSolver

Inherited from ConfigurationAnalyzer

Inherited from Analyser

Inherited from AnyRef

Inherited from Any

Ungrouped