Case class encoding the choice over a substitution varaible
Case class encoding the choice over a substitution varaible
the substitution variable
the value of the variable
type representing a clause as a set of predicate
type representing a clause as a set of predicate
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
Base trait for model predicates
Base trait for model predicates
Util case class for negation of Safety predicates
Util case class for negation of Safety predicates
the safety predicate to negate
Class encoding instance identifiers which can be ordered
Class encoding instance identifiers which can be ordered
Class encoding of component traces which can be ordered
Class encoding of component traces which can be ordered
Class encoding scala Symbol that can be compared
Class encoding scala Symbol that can be compared
Case class encoding the order requirement predicate
Case class encoding the order requirement predicate
the STMDD representing the system
the order requirement
Case class encoding the reliability requirement predicate
Case class encoding the reliability requirement predicate
the STMDD representing the system
the reliability requirement
Base trait for safety theory predicates
Base trait for safety theory predicates
Base trait for requirement predicates
Base trait for requirement predicates
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
Companion object for ordered instance identifiers
Companion object for ordered instance identifiers
Companion object of component traces
Companion object of component traces
Companion object for ordered symbols
Companion object for ordered symbols
Solver object handling classic Z3 Boolean assertions and custom Safety assertions
Solver object handling classic Z3 Boolean assertions and custom Safety assertions
Decision procedure of the Safety theory
Decision procedure of the Safety theory
the conjonction of Safety predicate on which the satisfiability modulo Safety must be decided
use quickXplain conflict clause minimisation
a model if SAT or a conflict clause if UNSAT
Order over flow identifiers
Order over flow identifiers
Order over constants
Order over constants
Order over instance identifiers in a system component
Order over instance identifiers in a system component
Memoized computation of the unreliability of an STMDD according to a selection
Memoized computation of the unreliability of an STMDD according to a selection
Timed DSE resolution
Timed DSE resolution
Generate substitution variables for component instance in the system
Generate substitution variables for component instance in the system
list of substitution var
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
the STMDD concerned by the model
the model of the substitution variables
the selection sequence
solution of the DSE problem
solution of the DSE problem
Solve the DSE problem of the actual configuration conf
Solve the DSE problem of the actual configuration conf
use quickXlain conflict clause minimisation algorithm
solution if it exists
Solve the DSE problem using custom reliability and order requirements
Solve the DSE problem using custom reliability and order requirements
optional reliability requirement
optional order requirement
use quickXlain conflict clause minimisation algorithm
solution if it exists
Solve DSE method with custom requirements and a given method
Solve DSE method with custom requirements and a given method
resolution method
optionnal reliability requirement
optionnal order requirement
solution if any
Solve DSE problem using HIPHOPS
Solve DSE problem using HIPHOPS
reliability requirement if defined, otherwise optimised
Solution if at least one found by HIPHOPS
implicit transformation from Symbol to Ordered Symbol
implicit transformation from Symbol to Ordered Symbol
Scala Symbol
ordered symbol
Trait containing DSE problem resolution with HIPHOPS and SMT