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 label on the STMDD edges
Case class encoding the label on the STMDD edges
the STMDD of the system
the STMDD of the system
the MDD factory used to build the STMDD
the MDD factory used to build the STMDD
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
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
compute the cardinality of a substitution choice
compute the cardinality of a substitution choice
the substitution choice
the over, under and exact cardinality (if computable)
Recursively compute the cardinality of a mdd node according to a substitution choice which is card(node)=min_{s \in node.kids} (card(s.tr,choice(node))+card(s.son))
Recursively compute the cardinality of a mdd node according to a substitution choice which is card(node)=min_{s \in node.kids} (card(s.tr,choice(node))+card(s.son))
mdd node
substitution chocie
the over, under and exact cardinality (if computable)
Calcul une surapprox, sous approx et valeur reel (si le choix est complet) de la defiabilite
Calcul une surapprox, sous approx et valeur reel (si le choix est complet) de la defiabilite
choix de selection de substiution
une mesure de la defibailite
Theorie de la defiabilite qui renvoi pour un choix donnee le status et la clause de conflit si status est UNSAT sinon le choix initial.
Theorie de la defiabilite qui renvoi pour un choix donnee le status et la clause de conflit si status est UNSAT sinon le choix initial. On parcours l'arbre des traces avec un budget de defiabilite a depenser, on calcul donc les long des chemins une borne min, max et si possible reel de la defiabilite. Si au bout de l'evaluation d'un groupe de chemins la reponse est UNSAT alors on sait que le modele n'est pas satisfaisant. Dans le cas d'une valuation incomplete Si la surapprox est correcte le modele est correct, la sous approx est incorrect le modele est incorrect, sinon on ne sait pas.
si le modele satisfait ou non les contrainte et une clause de conflit (CNF)
cardinality theory which returns for a given substitution choice, the status and the propogation and conflicts.
cardinality theory which returns for a given substitution choice, the status and the propogation and conflicts. The theory try to dispatch on the trace tree a budget corresponding to the cardinality requirement. For cardinality since card(node)=min_{s \in node.kids} (card(s)+card(tr_{node \to s})), then if one path does not fulfill the requirement then the candidate does not fill the requirement. Since the substitution choice is not always complete, an over and under approximations of the budget are computed at each step.
cardinality requirement
subsitution choice
the status of the dispatch operation and the conflicts/propagations
implicit transformation from Symbol to Ordered Symbol
implicit transformation from Symbol to Ordered Symbol
Scala Symbol
ordered symbol