T-wise combinatorial test

Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

@@ -2,6 +2,7 @@
 using System.IO;
 using System.Linq;
 using Antlr4.Runtime;
+using Antlr4.Runtime.Tree;
 using Plang.Compiler.TypeChecker;
 using Plang.Compiler.TypeChecker.AST;
 using Plang.Compiler.TypeChecker.AST.Declarations;
@@ -71,6 +72,12 @@ public Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing)
                 $"try to modify a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
+        public Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, int twiseNum, int paramNum)
+        {
+            return IssueError(location,
+                $"invalid twise: wise-number({twiseNum}) should great equal than 2 and less equal than number of parameters ({paramNum}) at {locationResolver.GetLocation(testDecl.SourceLocation)}");
+        }
+
         public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)
         {
             return IssueError(location,

Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

@@ -1,6 +1,7 @@
 using System;
 using System.IO;
 using Antlr4.Runtime;
+using Antlr4.Runtime.Tree;
 using Plang.Compiler.TypeChecker.AST;
 using Plang.Compiler.TypeChecker.AST.Declarations;
 using Plang.Compiler.TypeChecker.AST.States;
@@ -29,6 +30,8 @@ Exception DuplicateStartState(
         Exception UndeclaredGlobalParam(ParserRuleContext location, string name);
 
         Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
+
+        Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, int twiseNum, int paramNum);
 
         Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
 

Src/PCompiler/CompilerCore/Parser/PLexer.g4

@@ -59,7 +59,9 @@ THIS      : 'this' ;
 TYPE      : 'type' ;
 VALUES    : 'values' ;
 VAR       : 'var' ;
-PARAM       : 'param' ;
+PARAM     : 'param' ;
+PAIRWISE  : 'pairwise' ;
+WISE      : 'wise' ;
 WHILE     : 'while' ;
 WITH      : 'with' ;
 CHOOSE    : 'choose' ;

Src/PCompiler/CompilerCore/Parser/PParser.g4

@@ -253,7 +253,9 @@ paramBody : name=iden IN value=seqLiteral
           ;
 param : LPAREN paramBody RPAREN;
 
-testDecl : TEST (PARAM globalParam=param)? (ASSUME assumeExpr=expr)? testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # SafetyTestDecl
+twise : (PAIRWISE | LPAREN IntLiteral WISE RPAREN);
+
+testDecl : TEST (PARAM globalParam=param)? (ASSUME assumeExpr=expr)? (twise)? testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # SafetyTestDecl
          | TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr REFINES modExpr SEMI  # RefinementTestDecl
          ;
 

Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/SafetyTest.cs

@@ -8,6 +8,9 @@ public class SafetyTest(ParserRuleContext sourceNode, string testName) : IPDecl
     {
         public string Main { get; set; }
         public IPModuleExpr ModExpr { get; set; }
+
+        // from 2 to the number of parameters
+        public int Twise { get; set; }
 
         // When there is no param expression, it fails back to normal test
         public IDictionary<string, List<IPExpr>> ParamExprMap { get; set; } = new Dictionary<string, List<IPExpr>>();

Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs

@@ -66,6 +66,26 @@ public static void PopulateAllModuleExprs(
                 {
                     test.AssumeExpr = exprVisitor.Visit(context.assumeExpr);
                 }
+
+                if (context.twise() == null)
+                {
+                    test.Twise = test.ParamExprMap.Count;
+                }
+                else
+                {
+                    if (context.twise().PAIRWISE() != null)
+                    {
+                        test.Twise = 2;
+                    } else if (context.twise().WISE() != null)
+                    {
+                        var t = int.Parse(context.twise().IntLiteral().GetText());
+                        if (!(2 <= t && t <= test.ParamExprMap.Count))
+                        {
+                            throw handler.InvalidTwise(context.twise(), test, t, test.ParamExprMap.Count);
+                        }
+                        test.Twise = t;
+                    }
+                }
             }
 
             foreach (var test in globalScope.RefinementTests)

Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs

@@ -1,13 +1,118 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using System.Threading;
 using Plang.Compiler.TypeChecker.AST;
 using Plang.Compiler.TypeChecker.AST.Declarations;
 
 namespace Plang.Compiler.TypeChecker;
 
 public abstract class ParamAssignment
 {
+
+    public static IEnumerable<IEnumerable<T>> DifferentCombinations<T>(IEnumerable<T> elements, int k)
+    {
+        var enumerable = elements as T[] ?? elements.ToArray();
+        return k == 0 ? [Array.Empty<T>()]
+            :
+            enumerable.SelectMany((e, i) =>
+                DifferentCombinations(enumerable.Skip(i + 1), k - 1).Select(c => (new[] {e}).Concat(c)));
+    }
+
+    private static Dictionary<int, T> EnumerableToIndexDict<T> (IEnumerable<T> l, Func<T, T> f)
+    {
+        return Enumerable.Range(0, l.Count()).Zip(l, (a, b) => new { a, b }).ToDictionary(x => x.a, x => f(x.b));
+    }
+    private static Dictionary<int, Dictionary<string, int>> MakeVectorMap(Dictionary<string, int> universe, int twise)
+    {
+        var vectorSet = new HashSet<Dictionary<string, int>>();
+        foreach (var param in DifferentCombinations(universe.Select(kv => kv.Key), twise))
+        {
+            var result = new List<Dictionary<string, int>> { new() };
+            foreach (var name in param)
+            {
+                var newResult = new List<Dictionary<string, int>>();
+                for (var i = 0; i < universe[name]; i++)
+                {
+                    var resultCopy = result.Select(dict => dict.ToDictionary(kv => kv.Key, kv => kv.Value)).ToList();
+                    foreach (var vector in resultCopy)
+                    {
+                        vector.Add(name, i);
+                    }
+                    newResult.AddRange(resultCopy);
+                }
+                result = newResult;
+            }
+            vectorSet.UnionWith(result);
+        }
+        return EnumerableToIndexDict(vectorSet, x => x);
+    }
+
+    private static Dictionary<int, HashSet<int>> MakeAssignmentCoverageMap(
+        Dictionary<int, Dictionary<string, int>> assignmentMap,
+        Dictionary<int, Dictionary<string, int>> vectorMap,
+        List<int> assignments)
+    {
+        var assignmentCoverageMap = new Dictionary<int, HashSet<int>>();
+        foreach (var assignment in assignments)
+        {
+            assignmentCoverageMap.Add(assignment, []);
+            foreach (var kv in vectorMap.Where(kv => kv.Value.All(assignmentMap[assignment].Contains)))
+            {
+                assignmentCoverageMap[assignment].Add(kv.Key);
+            }
+        }
+        return assignmentCoverageMap;
+    }
+
+    private static List<int> GreedyCoverageExplore(Dictionary<string, int> universe, List<Dictionary<string, int>> assignmentList, int twise)
+    {
+        var assignments = Enumerable.Range(0, assignmentList.Count).ToList();
+        if (twise == universe.Count) return assignments;
+        var vectorMap = MakeVectorMap(universe, twise);
+        var assignmentMap = EnumerableToIndexDict(assignmentList, x => x);
+        // Console.WriteLine($"twise({twise})");
+        // Console.WriteLine($"assignments({assignments.Count})");
+        // Console.WriteLine($"vectorMap({vectorMap.Count})");
+        // foreach (var (i, indexDic) in vectorMap)
+        // {
+        //     Console.WriteLine($"vectorMap: {i}: {string.Join(',', indexDic)}");
+        // }
+        var assignmentCoverageMap = MakeAssignmentCoverageMap(assignmentMap, vectorMap, assignments);
+        // foreach (var (indexDic, c) in assignmentCoverageMap)
+        // {
+        //     Console.WriteLine($"Coverage: {string.Join(',', indexDic)} :: {string.Join(',', c)}");
+        // }
+        var obligationSet = vectorMap.Keys.ToHashSet();
+        // Console.WriteLine($"init obligationSet: {string.Join(',', obligationSet)}");
+        obligationSet.IntersectWith(assignmentCoverageMap.SelectMany(kv => kv.Value));
+        // Console.WriteLine($"obligationSet: {string.Join(',', obligationSet)}");
+        // foreach (var i in obligationSet)
+        // {
+        //     Console.WriteLine($"Missing Coverage: {string.Join(',', vectorMap[i])}");
+        // }
+        foreach (var kv in assignmentCoverageMap)
+        {
+            assignmentCoverageMap[kv.Key].IntersectWith(obligationSet);
+        }
+        var result = new List<int>();
+        while (obligationSet.Count != 0)
+        {
+            var (ass, coverage)= assignmentCoverageMap.MaxBy(kv => kv.Value.Count);
+            // Console.WriteLine($"Missing Coverage: {string.Join(',', obligationSet)}");
+            // Console.WriteLine($"Max one({string.Join(',', ass)}) covers({coverage.Count}) {string.Join(',', coverage)}");
+            obligationSet.ExceptWith(coverage);
+            assignmentCoverageMap.Remove(ass);
+            foreach (var kv in assignmentCoverageMap)
+            {
+                assignmentCoverageMap[kv.Key].ExceptWith(coverage);
+            }
+            result.Add(ass);
+        }
+        // Console.WriteLine($"result({result.Count})");
+        return result;
+    }
+
     private static Dictionary<string, IPExpr> Dic2StrDic(Dictionary<Variable, IPExpr> dic)
     {
         var dicAux = new Dictionary<string, IPExpr>();
@@ -56,15 +161,35 @@ public static void IterateAssignments(SafetyTest safety, List<Variable> globalPa
     {
         // Console.WriteLine($"safety.ParamExpr.Count = {safety.ParamExpr.Count}");
         var indexArr = safety.ParamExprMap.ToList().Zip(Enumerable.Repeat(0, safety.ParamExprMap.Count), (x, y) => (x.Key, y)).ToArray();
+        var universe = safety.ParamExprMap.ToDictionary(kv => kv.Key, kv => kv.Value.Count);
+        var assignmentIndices = new List<Dictionary<string, int>>();
         do
         {
             var indexDic = indexArr.ToDictionary(item => item.Item1, item => item.Item2);
             var dic = IndexDic2Dic(globalParams, safety.ParamExprMap, indexDic);
-            // Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr}");
-            // Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr} = {ForceBool(Eval(dic, safety.AssumeExpr))}");
-            if (!SimpleExprEval.ForceBool(SimpleExprEval.Eval(dic, safety.AssumeExpr))) continue;
-            // Console.WriteLine($"indexArr: {string.Join(',', indexArr)}");
-            f(dic);
+            if (!SimpleExprEval.ForceBool(SimpleExprEval.Eval(dic, safety.AssumeExpr)))
+            {
+                // Console.WriteLine($"UnSat Assumption: indexArr: {string.Join(',', indexArr)}");
+                continue;
+            }
+            assignmentIndices.Add(indexDic);
+            // Console.WriteLine($"Sat Assumption: indexArr: {string.Join(',', indexArr)}");
         } while (Next(indexArr, safety.ParamExprMap));
+
+        foreach (var i in GreedyCoverageExplore(universe, assignmentIndices, safety.Twise))
+        {
+            // Console.WriteLine($"Choose {safety.Twise}-wise: indexArr: {string.Join(',', assignmentIndices[i])}");
+            f(IndexDic2Dic(globalParams, safety.ParamExprMap, assignmentIndices[i]));
+        }
+        // do
+        // {
+        //     var indexDic = indexArr.ToDictionary(item => item.Item1, item => item.Item2);
+        //     var dic = IndexDic2Dic(globalParams, safety.ParamExprMap, indexDic);
+        //     // Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr}");
+        //     // Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr} = {ForceBool(Eval(dic, safety.AssumeExpr))}");
+        //     if (!SimpleExprEval.ForceBool(SimpleExprEval.Eval(dic, safety.AssumeExpr))) continue;
+        //     // Console.WriteLine($"indexArr: {string.Join(',', indexArr)}");
+        //     f(dic);
+        // } while (Next(indexArr, safety.ParamExprMap));
     }
 }

Tst/TestParamTester/1_ClientServer/PTst/Testscript.p

@@ -29,6 +29,25 @@ test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false
   assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
   (union Client, Bank, { TestWithConfig });
 
+  test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false]) 
+      assume (b1 == (nClients + g1 > g2)) 
+      (4 wise) testTWise4 [main=TestWithConfig]:
+  assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
+  (union Client, Bank, { TestWithConfig });
+
+  test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false]) 
+      assume (b1 == (nClients + g1 > g2)) 
+      (3 wise) testTWise3 [main=TestWithConfig]:
+  assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
+  (union Client, Bank, { TestWithConfig });
+
+  test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false]) 
+      assume (b1 == (nClients + g1 > g2)) 
+      (2 wise) testTWise2 [main=TestWithConfig]:
+  assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
+  (union Client, Bank, { TestWithConfig });
+
+
 // Syntax error
 // paramtest () wrong1 [main=TestWithSingleClient]:
 //   assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in