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

@@ -8,32 +8,107 @@ namespace Plang.Compiler.TypeChecker;
 
 public abstract class ParamAssignment
 {
-    private static Dictionary<string, IPExpr> Dic2StrDic(Dictionary<Variable, IPExpr> dic)
+    private static IEnumerable<IEnumerable<T>> DifferentCombinations<T>(IEnumerable<T> elements, int k)
     {
-        var dicAux = new Dictionary<string, IPExpr>();
-        foreach (var (k, i) in dic)
+        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)
         {
-            dicAux[k.Name] = i;
+            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);
+        var assignmentCoverageMap = MakeAssignmentCoverageMap(assignmentMap, vectorMap, assignments);
+        var obligationSet = vectorMap.Keys.ToHashSet();
+        obligationSet.IntersectWith(assignmentCoverageMap.SelectMany(kv => kv.Value));
+        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);
+            obligationSet.ExceptWith(coverage);
+            assignmentCoverageMap.Remove(ass);
+            foreach (var kv in assignmentCoverageMap) assignmentCoverageMap[kv.Key].ExceptWith(coverage);
+            result.Add(ass);
+        }
+
+        return result;
+    }
+
+    private static Dictionary<string, IPExpr> Dic2StrDic(Dictionary<Variable, IPExpr> dic)
+    {
+        var dicAux = new Dictionary<string, IPExpr>();
+        foreach (var (k, i) in dic) dicAux[k.Name] = i;
         return dicAux;
     }
 
-    private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalParams, IDictionary<string, List<IPExpr>> paramExprDic, IDictionary<string, int> indexDic)
+    private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalParams,
+        IDictionary<string, List<IPExpr>> paramExprDic, IDictionary<string, int> indexDic)
     {
         var dic = new Dictionary<Variable, IPExpr>();
         foreach (var (k, i) in indexDic)
         {
             var values = paramExprDic[k];
             var variable = globalParams.First(v => v.Name == k);
-            if (i >= values.Count)
-            {
-                throw new ArgumentException("Index out of range in global variable config."); 
-            }
+            if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config.");
             dic[variable] = values[i];
         }
+
         return dic;
     }
-    
+
     public static string RenameSafetyTestByAssignment(string name, Dictionary<Variable, IPExpr> dic)
     {
         var postfix = $"{string.Join("__", Dic2StrDic(dic).ToList().Select(p => $"{p.Key}_{p.Value}"))}";
@@ -45,26 +120,29 @@ private static bool Next((string, int)[] indexArr, IDictionary<string, List<IPEx
         for (var i = 0; i < indexArr.Length; i++)
         {
             indexArr[i] = (indexArr[i].Item1, indexArr[i].Item2 + 1);
-            // Console.WriteLine($"globalParams[globalVariables[{i}].Name].Count = {globalParams[globalVariables[i].Name].Count}");
             if (indexArr[i].Item2 < globalParams[indexArr[i].Item1].Count) return true;
             indexArr[i] = (indexArr[i].Item1, 0);
         }
+
         return false;
     }
 
-    public static void IterateAssignments(SafetyTest safety, List<Variable> globalParams, Action<Dictionary<Variable, IPExpr>> f)
+    public static void IterateAssignments(SafetyTest safety, List<Variable> globalParams,
+        Action<Dictionary<Variable, IPExpr>> f)
     {
-        // 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 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);
+            assignmentIndices.Add(indexDic);
         } while (Next(indexArr, safety.ParamExprMap));
+
+        foreach (var i in GreedyCoverageExplore(universe, assignmentIndices, safety.Twise))
+            f(IndexDic2Dic(globalParams, safety.ParamExprMap, assignmentIndices[i]));
     }
 }

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