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)
Created by kdelmas on 14/04/16.
(Since version KCR analyser 1.0) old version of safety theory