T-wise combinatorial (Solved Concerns from Lewis) (#838)

* Solved Concerns from Lewis:

+ new allow twise number be 1
+ unify twise number valid condition
+ add unit test

* add new test case

* unit test for ParamAssignment.IterateAssignments

Author: zhezhouzz

Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

@@ -72,10 +72,10 @@ 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)
+        public Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, string errMsg)
         {
             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)}");
+                $"invalid twise number at {locationResolver.GetLocation(testDecl.SourceLocation)}: {errMsg}");
         }
 
         public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)

Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

@@ -31,7 +31,7 @@ Exception DuplicateStartState(
 
         Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
 
-        Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, int twiseNum, int paramNum);
+        Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, string errMsg);
 
         Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
 

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

@@ -12,6 +12,11 @@ public Variable(string name, ParserRuleContext sourceNode, VariableRole role)
             SourceLocation = sourceNode;
             Role = role;
         }
+        
+        public Variable(string name)
+        {
+            Name = name;
+        }
 
         public VariableRole Role { get; }
         public PLanguageType Type { get; set; }

Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs

@@ -60,13 +60,12 @@ public static void PopulateAllModuleExprs(
                 if (context.globalParam != null)
                 {
                     var expr = (NamedTupleExpr)paramExprVisitor.Visit(context.globalParam);
-                    test.ParamExprMap = EnumerateParamAssignments (handler, globalScope, context.globalParam, expr);
+                    test.ParamExprMap = EnumerateParamAssignments(handler, globalScope, context.globalParam, expr);
                 }
                 if (context.assumeExpr != null)
                 {
                     test.AssumeExpr = exprVisitor.Visit(context.assumeExpr);
                 }
-
                 if (context.twise() == null)
                 {
                     test.Twise = test.ParamExprMap.Count;
@@ -76,12 +75,14 @@ public static void PopulateAllModuleExprs(
                     if (context.twise().PAIRWISE() != null)
                     {
                         test.Twise = 2;
-                    } else if (context.twise().WISE() != null)
+                    }
+                    else if (context.twise().WISE() != null)
                     {
                         var t = int.Parse(context.twise().IntLiteral().GetText());
-                        if (!(2 <= t && t <= test.ParamExprMap.Count))
+                        var (isValid, errMsg) = ParamAssignment.TwiseNumWellFormednessCheck(t, test.ParamExprMap.Count);
+                        if (!isValid)
                         {
-                            throw handler.InvalidTwise(context.twise(), test, t, test.ParamExprMap.Count);
+                            throw handler.InvalidTwise(context.twise(), test, errMsg);
                         }
                         test.Twise = t;
                     }

Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs

@@ -8,13 +8,28 @@ namespace Plang.Compiler.TypeChecker;
 
 public abstract class ParamAssignment
 {
-    private static IEnumerable<IEnumerable<T>> DifferentCombinations<T>(IEnumerable<T> elements, int k)
+    private static IEnumerable<IEnumerable<T>> DifferentCombinationsAux<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)));
+                DifferentCombinationsAux(enumerable.Skip(i + 1), k - 1).Select(c => new[] { e }.Concat(c)));
+    }
+
+    public static HashSet<HashSet<T>> DifferentCombinations<T>(IEnumerable<T> elements, int k)
+    {
+        var res = DifferentCombinationsAux(elements, k);
+        return new HashSet<HashSet<T>>(res.Select(innerEnumerable => new HashSet<T>(innerEnumerable)),
+            HashSet<T>.CreateSetComparer());
+    }
+
+    // Should use sum type (Option) instead of product type
+    public static (bool, string) TwiseNumWellFormednessCheck(int twise, int numParams)
+    {
+        return twise < 1
+            ? (false, $"twise number {twise} is less than 1.")
+            : (twise > numParams ? (false, $"twise number {twise} is greater than {numParams}.") : (true, ""));
     }
 
     private static Dictionary<int, T> EnumerableToIndexDict<T>(IEnumerable<T> l, Func<T, T> f)
@@ -37,19 +52,15 @@ private static Dictionary<int, Dictionary<string, int>> MakeVectorMap(Dictionary
                     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,
+        Dictionary<int, Dictionary<string, int>> assignmentMap, Dictionary<int, Dictionary<string, int>> vectorMap,
         List<int> assignments)
     {
         var assignmentCoverageMap = new Dictionary<int, HashSet<int>>();
@@ -59,7 +70,6 @@ private static Dictionary<int, HashSet<int>> MakeAssignmentCoverageMap(
             foreach (var kv in vectorMap.Where(kv => kv.Value.All(assignmentMap[assignment].Contains)))
                 assignmentCoverageMap[assignment].Add(kv.Key);
         }
-
         return assignmentCoverageMap;
     }
 
@@ -83,7 +93,6 @@ private static List<int> GreedyCoverageExplore(Dictionary<string, int> universe,
             foreach (var kv in assignmentCoverageMap) assignmentCoverageMap[kv.Key].ExceptWith(coverage);
             result.Add(ass);
         }
-
         return result;
     }
 
@@ -105,7 +114,6 @@ private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalPa
             if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config.");
             dic[variable] = values[i];
         }
-
         return dic;
     }
 
@@ -123,12 +131,11 @@ private static bool Next((string, int)[] indexArr, IDictionary<string, List<IPEx
             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)
+        Action<Dictionary<Variable, IPExpr>> generateTestCode)
     {
         var indexArr = safety.ParamExprMap.ToList()
             .Zip(Enumerable.Repeat(0, safety.ParamExprMap.Count), (x, y) => (x.Key, y)).ToArray();
@@ -141,8 +148,7 @@ public static void IterateAssignments(SafetyTest safety, List<Variable> globalPa
             if (!SimpleExprEval.ForceBool(SimpleExprEval.Eval(dic, safety.AssumeExpr))) continue;
             assignmentIndices.Add(indexDic);
         } while (Next(indexArr, safety.ParamExprMap));
-
         foreach (var i in GreedyCoverageExplore(universe, assignmentIndices, safety.Twise))
-            f(IndexDic2Dic(globalParams, safety.ParamExprMap, assignmentIndices[i]));
+            generateTestCode(IndexDic2Dic(globalParams, safety.ParamExprMap, assignmentIndices[i]));
     }
 }

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

@@ -47,6 +47,12 @@ 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)) 
+  (1 wise) testTWise1 [main=TestWithConfig]:
+assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
+(union Client, Bank, { TestWithConfig });
+
 
 // Syntax error
 // paramtest () wrong1 [main=TestWithSingleClient]:

Tst/UnitTests/TypeChecker/ParamAssignmentTest.cs

@@ -0,0 +1,86 @@
+using System.Collections.Generic;
+using System.Linq;
+using NUnit.Framework;
+using Plang.Compiler.TypeChecker;
+using Plang.Compiler.TypeChecker.AST;
+using Plang.Compiler.TypeChecker.AST.Declarations;
+using Plang.Compiler.TypeChecker.AST.Expressions;
+
+namespace UnitTests.TypeChecker;
+
+[TestFixture]
+[TestOf(typeof(ParamAssignment))]
+public class ParamAssignmentTest
+{
+    [Test]
+    public void TestDifferentCombinations()
+    {
+        var input = new List<int> { 1, 2, 3 };
+        var expected = new HashSet<HashSet<int>> { new() { 1, 2 }, new() { 1, 3 }, new() { 2, 3 } };
+        Assert.AreEqual(ParamAssignment.DifferentCombinations(input, 2), expected);
+        expected = [new HashSet<int> { 1 }, new HashSet<int> { 2 }, new HashSet<int> { 3 }];
+        Assert.AreEqual(ParamAssignment.DifferentCombinations(input, 1), expected);
+        expected = [new HashSet<int> { 1, 2, 3 }];
+        Assert.AreEqual(ParamAssignment.DifferentCombinations(input, 3), expected);
+    }
+
+    private static Dictionary<string, int> MakeSingleAssignment(int a, int b, int c)
+    {
+        return new Dictionary<string, int> { { "a", a }, { "b", b }, { "c", c } };
+    }
+
+    private static HashSet<Dictionary<string, int>> MakeExpectAssignments(int i)
+    {
+        return i switch
+        {
+            1 => // Total 3 obligations
+            [
+                MakeSingleAssignment(1, 1, 1), MakeSingleAssignment(2, 2, 2), MakeSingleAssignment(1, 3, 1)
+            ],
+            2 => // Total 2*3 + 2*2 + 3*2 = 16 obligations
+            [
+                MakeSingleAssignment(1, 1, 1), // (a = 1, b = 1) (a = 1, c = 1) (b = 1, c = 1)
+                MakeSingleAssignment(2, 2, 1), // (a = 2, b = 2) (a = 2, c = 1) (b = 2, c = 1)
+                MakeSingleAssignment(2, 1, 2), // (a = 2, b = 1) (a = 2, c = 2) (b = 1, c = 2)
+                MakeSingleAssignment(1, 2, 2), // (a = 1, b = 2) (a = 1, c = 2) (b = 2, c = 2)
+                MakeSingleAssignment(1, 3, 1), // (a = 1, b = 3) (b = 3, c = 1)
+                MakeSingleAssignment(2, 3, 2)  // (a = 2, b = 3) (b = 3, c = 2)
+            ],
+            3 => // Total 2*3*2 = 12 obligations, need all combinations
+            [
+                MakeSingleAssignment(1, 1, 1), MakeSingleAssignment(2, 1, 1), MakeSingleAssignment(1, 2, 1),
+                MakeSingleAssignment(2, 2, 1), MakeSingleAssignment(1, 3, 1), MakeSingleAssignment(2, 3, 1),
+                MakeSingleAssignment(1, 1, 2), MakeSingleAssignment(2, 1, 2), MakeSingleAssignment(1, 2, 2),
+                MakeSingleAssignment(2, 2, 2), MakeSingleAssignment(1, 3, 2), MakeSingleAssignment(2, 3, 2),
+            ],
+            _ => []
+        };
+    }
+
+    [Test]
+    public void TestIterateAssignments()
+    {
+        var safety = new SafetyTest(null, "test")
+        {
+            ParamExprMap = new Dictionary<string, List<IPExpr>>
+            {
+                { "a", [new IntLiteralExpr(1), new IntLiteralExpr(2)] },
+                { "b", [new IntLiteralExpr(1), new IntLiteralExpr(2), new IntLiteralExpr(3)] },
+                { "c", [new IntLiteralExpr(1), new IntLiteralExpr(2)] },
+            },
+            AssumeExpr = new BoolLiteralExpr(true),
+            Twise = 0
+        };
+        var globalParams = safety.ParamExprMap.Select(kv => new Variable(kv.Key)).ToList();
+        for (var i = 1; i <= 3; i++)
+        {
+            safety.Twise = i;
+            var nativeRecord = new HashSet<Dictionary<Variable, IPExpr>>();
+            ParamAssignment.IterateAssignments(safety, globalParams, dict => nativeRecord.Add(dict));
+            var record = nativeRecord
+                .Select(dict => dict.ToDictionary(kv => kv.Key.Name, kv => ((IntLiteralExpr)kv.Value).Value))
+                .ToHashSet();
+            Assert.AreEqual(record, MakeExpectAssignments(i));
+        }
+    }
+}