Open FAMILIAR-project opened 11 years ago
In FMLDisjunctiveSATMergerTest
test1()
_shell.parse("// with explicity negated variables\n" + "fm1 = FM (A : [B] [C] [E] [F] ; !E ; !F ; ) \n" + "fm2 = FM (A : [B] [E] [F] ; B : C ; !E ; )\n" + "fm3 = FM (A : B [F] [E] [C] ; !F ; !C ; )");
List<FeatureModelVariable> fmvs = new ArrayList<FeatureModelVariable>() ;
FeatureModelVariable fm1 = getFMVariable("fm1") ;
System.err.println("eg fm1 = " + fm1.computeExcludesEdge());
eg fm1 = [(C -> !E), (B -> !E), (A -> !F), (B -> !F), (A -> !E), (C -> !F)]
why E -> !F does not appear is strange
System.err.println("eg fm1 (bis)" + new SATFMLFormula(fm1).computeExclusionGraph(fm1.features().names()));
eg fm1 (bis)(E -> !F) (E -> !A) (E -> !B) (E -> !C) (F -> !A) (F -> !B) (F -> !C)
so SAT-based is OK
fml> fm1 fm1: (FEATURE_MODEL) A: [B] [E] [C] [F] ; !E; !F; fml> i1 = computeImplies fm1 i1: (SET) {(C -> A);(E -> B);(B -> A);(E -> A);(F -> B);(E -> C);(E -> F);(F -> C);(F -> A);(F -> E)}
E -> F should not be included !?
fml> e1 = computeExcludes fm1 e1: (SET) {(B -> !F);(A -> !F);(C -> !E);(A -> !E);(B -> !E);(C -> !F)}
E -> !F should be included !?