Package

util

analyzers

Permalink

package analyzers

Visibility
  1. Public
  2. All

Type Members

  1. class Alternative extends AnyRef

    Permalink

    class representing a component alternative for the SMT based analysis

  2. trait AlternativeAnalyzer extends Analyser

    Permalink
  3. trait AlternativesAnalyser extends Analyser

    Permalink

    Analysis of the alternatives for a given design space

  4. trait AnalyzerExceptions extends Exception

    Permalink
  5. trait BDDAnalyzer extends AnyRef

    Permalink

    Created by kdelmas on 04/11/16.

  6. trait BDDBuild extends PhiAnalyzer

    Permalink

    Trait for encoding structure function as a BDD

  7. class BDDFactory extends BaseBDDFactory[Int, BDD]

    Permalink

    Class for a classic BDD Factory (variable are integer and BDD are JavaBDD)

  8. trait BDDFactoryField extends AnyRef

    Permalink

    Created by kdelmas on 27/09/17.

  9. case class BadOrdering[Var](father: Var, son: Var) extends Exception with MDDException with Product with Serializable

    Permalink
  10. trait BaseBDDFactory[Var, MyBDD <: BDD] extends AnyRef

    Permalink

    base trait for BDD factories

    base trait for BDD factories

    Var

    the type of variable labelled on BDD nodes

    MyBDD

    the BDD representation which must be a subtype of JavaBDD type

  11. trait Bounded[T] extends AnyRef

    Permalink
  12. trait CardinalityAnalysis extends PhiAnalyzer

    Permalink

    Trait for order computation

  13. case class CharacteristicFun[T](func: Map[Map[BasicFlowIdent, BitVecNum], T], default: T) extends Product with Serializable

    Permalink

    Case class encoding a partial function over component traces

    Case class encoding a partial function over component traces

    T

    the type of return values

    func

    the function from component trace to value

    default

    the default value

  14. class Component extends AnyRef

    Permalink

    class representing a component for component analysis by SMT-based approach

  15. trait ComponentAnalyzer extends Analyser

    Permalink

    Created by kdelmas on 08/04/16.

  16. trait Console extends AnyRef

    Permalink
  17. trait CutComputationMode extends AnyRef

    Permalink

    Base trait for available cut computation modes

  18. trait DelegatedConsole extends Console

    Permalink
  19. trait DesignSpaceExplorationMethod extends AnyRef

    Permalink

    Base trait for available DSE resolution methods

  20. sealed trait DslLit extends AnyRef

    Permalink

    Base type for literals in prime implicants, in terms of DSL identifiers.

  21. case class ExecutionTimes(preProcessTime: Long, processTime: Long, postProcessTime: Long) extends Product with Serializable

    Permalink

    Created by kevin on 15/02/17.

  22. trait ExtractorListP[E <: NodeListP[K, P], P, K <: Node] extends AnyRef

    Permalink

    Extractor from parameter node

    Extractor from parameter node

    E

    the type of the node

    P

    the type of parameter

    K

    the type of the kids

  23. trait ExtractorNP[E <: NodeNP[K, V, P], K, P, V <: Node] extends AnyRef

    Permalink

    Extractor from parameter node

    Extractor from parameter node

    E

    the type of the node

    K

    the type of edge label

    P

    the type of parameter

    V

    the type of kids

  24. trait ExtractorP[E <: NodeP[P], P] extends AnyRef

    Permalink

    Extractor from parameter node

    Extractor from parameter node

    E

    the node type

    P

    the parameter type

  25. trait FBDDBuild extends ComponentAnalyzer

    Permalink

    compute the BDD of the trigger function of each possible trace of the component

  26. trait FBDDBuildSMT extends FBDDBuild

    Permalink
  27. trait FCardinalityBuild extends ComponentAnalyzer with BDDAnalyzer

    Permalink

    compute the cardinality of BDD trigger functions of the component

  28. trait FUnreliabilityBuild extends BDDAnalyzer

    Permalink
  29. trait Factory[E] extends AnyRef

    Permalink

    Base trait for node factory based on hashConsing

    Base trait for node factory based on hashConsing

    E

    the type of the nodes

  30. trait FactoryListP[T, E <: T with NodeListP[K, P], P, K <: Node] extends Factory[E]

    Permalink

    Factory for node containing list of kids

    Factory for node containing list of kids

    T

    the type of simplified node

    E

    the type of the nodes

    P

    the type of the parameter

    K

    the type of kids

  31. trait FactoryNP[T, E <: T with NodeNP[K, V, P], K, P, V <: Node, M[K, V] <: Map[K, V]] extends Factory[E]

    Permalink

    Hashcode computation for leaf node

    Hashcode computation for leaf node

    T

    the type of reduced nodes

    E

    the type of the nodes

    K

    the type of edge labels

    P

    the type of the parameter

    V

    the type of the kids

    M

    the type of the collection gathering kids

  32. trait FactoryP[E <: NodeP[P], P] extends Factory[E]

    Permalink

    Factory for nodes containing only a parameter

    Factory for nodes containing only a parameter

    E

    the type of the nodes

    P

    the type of parameter

  33. trait GenBDDFactory[Var] extends BaseBDDFactory[Var, BDD]

    Permalink

    Generic BDD factory over the type of BDD variables

    Generic BDD factory over the type of BDD variables

    Var

    the type of variable labelled on BDD nodes

  34. trait GenMDDFactory[Var <: Ordered[Var], F[V] <: Traversable[V], Val <: Ordered[Val], TL <: Ordered[TL], Dom] extends AnyRef

    Permalink

    Base trait for MDD factory

    Base trait for MDD factory

    Var

    Variable type

    F

    collection type for values

    Val

    values type

    TL

    terminal type

    Dom

    variables' domain type

  35. case class IllegalSubstitution(compInst: CompInstanceIdent, sub: CompIdent, trace: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  36. case class InclusionSet[T <: Set[E], E](holder: Set[T] = Set[T]()) extends Set[T] with Product with Serializable

    Permalink

    Case class encoding Set of Sets and ensuring that any element cannot be contained in another one

    Case class encoding Set of Sets and ensuring that any element cannot be contained in another one

    T

    the element type, must be subtype of Set

    E

    the type of Set elements

    holder

    initial set

  37. case class InfNumeric[T] extends Ordered[InfNumeric[T]] with Product with Serializable

    Permalink

    Case class representing infinite numeric (classic number plus infinity)

    Case class representing infinite numeric (classic number plus infinity)

    T

    the type of the values

  38. trait InfNumericIsNumeric[T] extends Numeric[InfNumeric[T]]

    Permalink

    Base trait used to defined Numeric implicit objects

    Base trait used to defined Numeric implicit objects

    T

    the type of the values

  39. sealed trait Infinity extends AnyRef

    Permalink

    Base trait for representing infinite values

  40. class InstBoolBDDFactory extends GenBDDFactory[InstBoolIdent]

    Permalink

    BDDFactory where variables labelled on BDD node are InstBoolIdent

  41. class IterativeMCSEnumerator extends AnyRef

    Permalink

    Translates the structure function of a system represented by a z3 expression to a SAT-solver friendly formula in DIMACS or OPB format for prime implicant enumeration using external solvers.

  42. trait LegalAnalyser extends Analyser

    Permalink

    Legality analysis based on SMT problem solving

  43. sealed trait MDDException extends Exception

    Permalink
  44. class MDDFactory[Var <: Ordered[Var], F[V] <: Traversable[V], Val <: Ordered[Val], TL <: Ordered[TL], Dom] extends GenMDDFactory[Var, F, Val, TL, Dom]

    Permalink

    MDD factory class

    MDD factory class

    Var

    Variable type

    F

    collection type for values

    Val

    values type

    TL

    terminal type

    Dom

    variables' domain type

  45. trait MDDPrinter[Var <: Ordered[Var], F[V] <: Traversable[V], Val <: Ordered[Val], TL <: Ordered[TL], Dom] extends AnyRef

    Permalink

    Printer trait should be mixed with a factory

    Printer trait should be mixed with a factory

    Var

    the type representing node variables

    F

    the collection types of values associated to a variable

    Val

    the type of variables possible values

  46. class Measure[T] extends AnyRef

    Permalink

    Interval approximation of numeric values

    Interval approximation of numeric values

    T

    the type of the value

  47. case class MissingBaseAlternative(compInstanceIdent: DSLSymbol) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  48. case class MissingSubstitution(compInstanceIdent: CompInstanceIdent) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  49. case class MonotonyCounterExample(events: Map[InstBoolIdent, (Expr, Expr)]) extends Product with Serializable

    Permalink
  50. sealed abstract class MyMemo[K, V] extends AnyRef

    Permalink

    Created by kdelmas on 16/11/16.

  51. case class NegDslLit(ident: InstBoolIdent) extends DslLit with Product with Serializable

    Permalink

    A negative literal.

  52. trait Node extends AnyRef

    Permalink
  53. trait NodeListP[K <: Node, P] extends Node

    Permalink
  54. trait NodeNP[K, V <: Node, P] extends Node

    Permalink
  55. trait NodeP[P] extends Node

    Permalink
  56. case class OutOfVariableRange(domainsSize: Int, index: Int) extends Exception with MDDException with Product with Serializable

    Permalink
  57. class PBMCSEnumerator extends AnyRef

    Permalink

    Translates the structure function of a system represented by a z3 expression to a SAT-solver friendly formula in DIMACS or OPB format for prime implicant enumeration using external solvers.

  58. case class ParsingFailure(cause: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  59. case class Phi(expr: BoolExpr, events: DSLEventToZ3Map, context: SMTContext) extends Product with Serializable

    Permalink

    Case class encoding the structure function of a system

    Case class encoding the structure function of a system

    expr

    the boolean expression of the structure function

    events

    the mapping of KCR events to Z3 varaibles

    context

    the SMT evaluation context

  60. trait PhiAnalyzer extends Analyser

    Permalink

    Base trait for analysis of the structure function

  61. trait PhiCutEnumeration[R] extends PhiAnalyzer

    Permalink

    Trait fot cutsets computation on phi

    Trait fot cutsets computation on phi

    R

    the collection to store cutsets

  62. trait PhiCutEnumerationBDD extends PhiCutEnumeration[InstBoolIdent] with BDDAnalyzer

    Permalink

    Trait for BDD based cutsets enumeration on phi

  63. trait PhiCutEnumerationIterativeSAT extends PhiCutEnumeration[InstBoolIdent]

    Permalink

    Trait for SAT based enumeration of cutsets

  64. trait PhiCutEnumerationIterativeSMT extends PhiCutEnumeration[InstBoolIdent]

    Permalink

    Trait for SMT resolution based cutsets enumeration

  65. trait PhiCutEnumerationPB extends PhiCutEnumeration[InstBoolIdent]

    Permalink

    Trait for Pseudo-Boolean based cutsets computation

  66. trait PhiCutEnumerationTREK extends PhiCutEnumeration[InstBoolIdent]

    Permalink
  67. case class PosDslLit(ident: InstBoolIdent) extends DslLit with Product with Serializable

    Permalink

    A positive literal.

  68. trait ProbLikeBound[T] extends Bounded[T]

    Permalink
  69. abstract class Profiler[I, O] extends AnyRef

    Permalink
  70. trait RelationBuild extends ComponentAnalyzer

    Permalink

    compute the SMT expression (c in1..inn e1..ek)=(o1..om) where flows and events are bounded variables

  71. sealed trait Sign extends AnyRef

    Permalink
  72. trait SolutionAnalyzer extends ConfigurationAnalyzer

    Permalink

    Trait for additional analysis of the DSE problem solution

  73. class Substitution extends AnyRef

    Permalink

    Case clas for subsitution analysis with pure SMT exploration (ie without the interpreter)

  74. case class SubstitutionVar(inst: CompInstanceIdent, z3Var: Expr, sort: EnumSort) extends Product with Serializable

    Permalink

    Case class encoding substitution variables

    Case class encoding substitution variables

    inst

    the targeted instance

    z3Var

    the corresponding Z3 variable

    sort

    the sort of the Z3 varaible

  75. trait SystemConsole extends Console

    Permalink
  76. class TREKPIEnumerator extends AnyRef

    Permalink

    Class for enumrating prime implicants of a structure function.

  77. class TimeoutTask[T] extends AnyRef

    Permalink

    Class for timeout task

    Class for timeout task

    T

    the type of returned result

  78. trait ToolInterface extends AnyRef

    Permalink
  79. case class ToolNotFound(msg: String) extends Exception with Product with Serializable

    Permalink

    Created by kdelmas on 22/02/17.

  80. trait TraceBuild extends ComponentAnalyzer

    Permalink

    compute the SMT expression (exists e1..ek (c in1..inn e1..ek)=(o1..om)) in traceFieldExpr where flows are given as bounded variables referred in traceFieldVars

  81. case class UndeterminedForm(computation: String) extends Exception with Product with Serializable

    Permalink
  82. case class UnknownEvent(eventName: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  83. case class UnknownInstance(compInstanceIdent: CompInstanceIdent) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  84. case class UnknownValue[Var, Val](variable: Var, value: Val) extends Exception with MDDException with Product with Serializable

    Permalink
  85. case class UnknownVariable[Var](variable: Var) extends Exception with MDDException with Product with Serializable

    Permalink
  86. case class UnknownZ3AST(node: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  87. case class WrongBDDSimplification(node: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  88. case class WrongBoolExpr(expression: String) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  89. trait Z3BoolExprToBDDTranslator extends Z3ExprTranslators

    Permalink

    Base trait for translating Z3 SMT Boolean expression to BDD

  90. trait Z3ExprTranslators extends AnyRef

    Permalink

    Created by kdelmas on 04/11/16.

  91. case class Z3UnknownException(analysis: Analyser) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink
  92. case class Z3UnsatException(analysis: Analyser) extends Exception with AnalyzerExceptions with Product with Serializable

    Permalink

Value Members

  1. object BDDCutComputation extends CutComputationMode

    Permalink

    Cut computation based on BDD analysis

  2. object CardMeasure

    Permalink
  3. object ClaspInterface extends ToolInterface

    Permalink
  4. object CygwinInterface extends ToolInterface

    Permalink
  5. object FactoryListP

    Permalink

    Factory for node containing list of kids

  6. object FactoryNP

    Permalink

    Factory for node containing parameter and a map of kids

  7. object FactoryP

    Permalink

    Factory for nodes containing only a parameter

  8. object GeneticExploration extends DesignSpaceExplorationMethod with Product with Serializable

    Permalink

    HIPHOPS based DSE resolution method

  9. object HipHOPSCutComputation extends CutComputationMode

    Permalink

    Cut enumeration based on HIPHOPS external tool

  10. object HipHOPSInterface extends ToolInterface

    Permalink
  11. object InfNumericImplicits

    Permalink

    Useful conversion from infinity to infinite numeric

  12. object InfNumericTypes

    Permalink

    Particular type of infinite numeric

  13. object IterativeSATCutComputation extends CutComputationMode

    Permalink

    Cut computation based on Iterative SAT method

  14. object IterativeSMTCutComputation extends CutComputationMode

    Permalink

    Cut computation based on Iterative SMT method

  15. object Measure

    Permalink
  16. object MeasureTypes

    Permalink

    Created by kdelmas on 04/11/16.

  17. object MyMemo

    Permalink
  18. object NEGATIVE extends Sign with Product with Serializable

    Permalink
  19. object NEGATIVE_INFINITY extends Infinity with Product with Serializable

    Permalink

    Object representing negative infinity

  20. object Node

    Permalink
  21. object PBCutComputation extends CutComputationMode

    Permalink

    Cut enumeration based on Pseudo-Boolean solving

  22. object PBEncoderInterface extends ToolInterface

    Permalink
  23. object POSITIVE extends Sign with Product with Serializable

    Permalink
  24. object POSITIVE_INFINITY extends Infinity with Product with Serializable

    Permalink

    Object representing positive infinity

  25. object ProbaMeasure

    Permalink
  26. object PythonInterface extends ToolInterface

    Permalink
  27. object SMTExploration extends DesignSpaceExplorationMethod with Product with Serializable

    Permalink

    SMT based resolution method

  28. object SharpCDCLInterface extends ToolInterface

    Permalink
  29. object TimeoutTask

    Permalink
  30. object WineInterface extends ToolInterface

    Permalink
  31. object XFTACutComputation extends CutComputationMode

    Permalink

    Cut enumeration based on XFTA external tool

  32. object XFTAInterface extends ToolInterface

    Permalink
  33. object XSAPCutComputation extends CutComputationMode

    Permalink

    Cut enumeration based on XSAP external tool

  34. object XSAPInterface extends ToolInterface

    Permalink
  35. object Z3ExprToFormulaLike

    Permalink

    Created by rdelmas on 07/06/16.

    Created by rdelmas on 07/06/16.

    A translation function from z3 expressions to FormulaLike

  36. object Z3JavaSO extends ToolInterface

    Permalink
  37. object ZERO extends Sign with Product with Serializable

    Permalink
  38. package analyzerTypes

    Permalink

Ungrouped