Skip to content

Commit c7e86ab

Browse files
zhezhouzzzhezhouzz
authored
T-wise combinatorial test (#837)
* add twise * clean the code
1 parent bd3d167 commit c7e86ab

File tree

8 files changed

+154
-20
lines changed

8 files changed

+154
-20
lines changed

‎Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
using System.IO;
33
using System.Linq;
44
using Antlr4.Runtime;
5+
using Antlr4.Runtime.Tree;
56
using Plang.Compiler.TypeChecker;
67
using Plang.Compiler.TypeChecker.AST;
78
using Plang.Compiler.TypeChecker.AST.Declarations;
@@ -71,6 +72,12 @@ public Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing)
7172
$"try to modify a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
7273
}
7374

75+
public Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, int twiseNum, int paramNum)
76+
{
77+
return IssueError(location,
78+
$"invalid twise: wise-number({twiseNum}) should great equal than 2 and less equal than number of parameters ({paramNum}) at {locationResolver.GetLocation(testDecl.SourceLocation)}");
79+
}
80+
7481
public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)
7582
{
7683
return IssueError(location,

‎Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
using System;
22
using System.IO;
33
using Antlr4.Runtime;
4+
using Antlr4.Runtime.Tree;
45
using Plang.Compiler.TypeChecker.AST;
56
using Plang.Compiler.TypeChecker.AST.Declarations;
67
using Plang.Compiler.TypeChecker.AST.States;
@@ -29,6 +30,8 @@ Exception DuplicateStartState(
2930
Exception UndeclaredGlobalParam(ParserRuleContext location, string name);
3031

3132
Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
33+
34+
Exception InvalidTwise(ParserRuleContext location, IPDecl testDecl, int twiseNum, int paramNum);
3235

3336
Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
3437

‎Src/PCompiler/CompilerCore/Parser/PLexer.g4

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,9 @@ THIS : 'this' ;
5959
TYPE : 'type' ;
6060
VALUES : 'values' ;
6161
VAR : 'var' ;
62-
PARAM : 'param' ;
62+
PARAM : 'param' ;
63+
PAIRWISE : 'pairwise' ;
64+
WISE : 'wise' ;
6365
WHILE : 'while' ;
6466
WITH : 'with' ;
6567
CHOOSE : 'choose' ;

‎Src/PCompiler/CompilerCore/Parser/PParser.g4

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,9 @@ paramBody : name=iden IN value=seqLiteral
253253
;
254254
param : LPAREN paramBody RPAREN;
255255

256-
testDecl : TEST (PARAM globalParam=param)? (ASSUME assumeExpr=expr)? testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # SafetyTestDecl
256+
twise : (PAIRWISE | LPAREN IntLiteral WISE RPAREN);
257+
258+
testDecl : TEST (PARAM globalParam=param)? (ASSUME assumeExpr=expr)? (twise)? testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # SafetyTestDecl
257259
| TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr REFINES modExpr SEMI # RefinementTestDecl
258260
;
259261

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,9 @@ public class SafetyTest(ParserRuleContext sourceNode, string testName) : IPDecl
88
{
99
public string Main { get; set; }
1010
public IPModuleExpr ModExpr { get; set; }
11+
12+
// from 2 to the number of parameters
13+
public int Twise { get; set; }
1114

1215
// When there is no param expression, it fails back to normal test
1316
public IDictionary<string, List<IPExpr>> ParamExprMap { get; set; } = new Dictionary<string, List<IPExpr>>();

‎Src/PCompiler/CompilerCore/TypeChecker/ModuleExprVisitor.cs

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,26 @@ public static void PopulateAllModuleExprs(
6666
{
6767
test.AssumeExpr = exprVisitor.Visit(context.assumeExpr);
6868
}
69+
70+
if (context.twise() == null)
71+
{
72+
test.Twise = test.ParamExprMap.Count;
73+
}
74+
else
75+
{
76+
if (context.twise().PAIRWISE() != null)
77+
{
78+
test.Twise = 2;
79+
} else if (context.twise().WISE() != null)
80+
{
81+
var t = int.Parse(context.twise().IntLiteral().GetText());
82+
if (!(2 <= t && t <= test.ParamExprMap.Count))
83+
{
84+
throw handler.InvalidTwise(context.twise(), test, t, test.ParamExprMap.Count);
85+
}
86+
test.Twise = t;
87+
}
88+
}
6989
}
7090

7191
foreach (var test in globalScope.RefinementTests)

‎Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs

Lines changed: 96 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -8,32 +8,107 @@ namespace Plang.Compiler.TypeChecker;
88

99
public abstract class ParamAssignment
1010
{
11-
private static Dictionary<string, IPExpr> Dic2StrDic(Dictionary<Variable, IPExpr> dic)
11+
private static IEnumerable<IEnumerable<T>> DifferentCombinations<T>(IEnumerable<T> elements, int k)
1212
{
13-
var dicAux = new Dictionary<string, IPExpr>();
14-
foreach (var (k, i) in dic)
13+
var enumerable = elements as T[] ?? elements.ToArray();
14+
return k == 0
15+
? [Array.Empty<T>()]
16+
: enumerable.SelectMany((e, i) =>
17+
DifferentCombinations(enumerable.Skip(i + 1), k - 1).Select(c => new[] { e }.Concat(c)));
18+
}
19+
20+
private static Dictionary<int, T> EnumerableToIndexDict<T>(IEnumerable<T> l, Func<T, T> f)
21+
{
22+
return Enumerable.Range(0, l.Count()).Zip(l, (a, b) => new { a, b }).ToDictionary(x => x.a, x => f(x.b));
23+
}
24+
25+
private static Dictionary<int, Dictionary<string, int>> MakeVectorMap(Dictionary<string, int> universe, int twise)
26+
{
27+
var vectorSet = new HashSet<Dictionary<string, int>>();
28+
foreach (var param in DifferentCombinations(universe.Select(kv => kv.Key), twise))
29+
{
30+
var result = new List<Dictionary<string, int>> { new() };
31+
foreach (var name in param)
32+
{
33+
var newResult = new List<Dictionary<string, int>>();
34+
for (var i = 0; i < universe[name]; i++)
35+
{
36+
var resultCopy = result.Select(dict => dict.ToDictionary(kv => kv.Key, kv => kv.Value)).ToList();
37+
foreach (var vector in resultCopy) vector.Add(name, i);
38+
newResult.AddRange(resultCopy);
39+
}
40+
41+
result = newResult;
42+
}
43+
44+
vectorSet.UnionWith(result);
45+
}
46+
47+
return EnumerableToIndexDict(vectorSet, x => x);
48+
}
49+
50+
private static Dictionary<int, HashSet<int>> MakeAssignmentCoverageMap(
51+
Dictionary<int, Dictionary<string, int>> assignmentMap,
52+
Dictionary<int, Dictionary<string, int>> vectorMap,
53+
List<int> assignments)
54+
{
55+
var assignmentCoverageMap = new Dictionary<int, HashSet<int>>();
56+
foreach (var assignment in assignments)
1557
{
16-
dicAux[k.Name] = i;
58+
assignmentCoverageMap.Add(assignment, []);
59+
foreach (var kv in vectorMap.Where(kv => kv.Value.All(assignmentMap[assignment].Contains)))
60+
assignmentCoverageMap[assignment].Add(kv.Key);
1761
}
62+
63+
return assignmentCoverageMap;
64+
}
65+
66+
private static List<int> GreedyCoverageExplore(Dictionary<string, int> universe,
67+
List<Dictionary<string, int>> assignmentList, int twise)
68+
{
69+
var assignments = Enumerable.Range(0, assignmentList.Count).ToList();
70+
if (twise == universe.Count) return assignments;
71+
var vectorMap = MakeVectorMap(universe, twise);
72+
var assignmentMap = EnumerableToIndexDict(assignmentList, x => x);
73+
var assignmentCoverageMap = MakeAssignmentCoverageMap(assignmentMap, vectorMap, assignments);
74+
var obligationSet = vectorMap.Keys.ToHashSet();
75+
obligationSet.IntersectWith(assignmentCoverageMap.SelectMany(kv => kv.Value));
76+
foreach (var kv in assignmentCoverageMap) assignmentCoverageMap[kv.Key].IntersectWith(obligationSet);
77+
var result = new List<int>();
78+
while (obligationSet.Count != 0)
79+
{
80+
var (ass, coverage) = assignmentCoverageMap.MaxBy(kv => kv.Value.Count);
81+
obligationSet.ExceptWith(coverage);
82+
assignmentCoverageMap.Remove(ass);
83+
foreach (var kv in assignmentCoverageMap) assignmentCoverageMap[kv.Key].ExceptWith(coverage);
84+
result.Add(ass);
85+
}
86+
87+
return result;
88+
}
89+
90+
private static Dictionary<string, IPExpr> Dic2StrDic(Dictionary<Variable, IPExpr> dic)
91+
{
92+
var dicAux = new Dictionary<string, IPExpr>();
93+
foreach (var (k, i) in dic) dicAux[k.Name] = i;
1894
return dicAux;
1995
}
2096

21-
private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalParams, IDictionary<string, List<IPExpr>> paramExprDic, IDictionary<string, int> indexDic)
97+
private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalParams,
98+
IDictionary<string, List<IPExpr>> paramExprDic, IDictionary<string, int> indexDic)
2299
{
23100
var dic = new Dictionary<Variable, IPExpr>();
24101
foreach (var (k, i) in indexDic)
25102
{
26103
var values = paramExprDic[k];
27104
var variable = globalParams.First(v => v.Name == k);
28-
if (i >= values.Count)
29-
{
30-
throw new ArgumentException("Index out of range in global variable config.");
31-
}
105+
if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config.");
32106
dic[variable] = values[i];
33107
}
108+
34109
return dic;
35110
}
36-
111+
37112
public static string RenameSafetyTestByAssignment(string name, Dictionary<Variable, IPExpr> dic)
38113
{
39114
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
45120
for (var i = 0; i < indexArr.Length; i++)
46121
{
47122
indexArr[i] = (indexArr[i].Item1, indexArr[i].Item2 + 1);
48-
// Console.WriteLine($"globalParams[globalVariables[{i}].Name].Count = {globalParams[globalVariables[i].Name].Count}");
49123
if (indexArr[i].Item2 < globalParams[indexArr[i].Item1].Count) return true;
50124
indexArr[i] = (indexArr[i].Item1, 0);
51125
}
126+
52127
return false;
53128
}
54129

55-
public static void IterateAssignments(SafetyTest safety, List<Variable> globalParams, Action<Dictionary<Variable, IPExpr>> f)
130+
public static void IterateAssignments(SafetyTest safety, List<Variable> globalParams,
131+
Action<Dictionary<Variable, IPExpr>> f)
56132
{
57-
// Console.WriteLine($"safety.ParamExpr.Count = {safety.ParamExpr.Count}");
58-
var indexArr = safety.ParamExprMap.ToList().Zip(Enumerable.Repeat(0, safety.ParamExprMap.Count), (x, y) => (x.Key, y)).ToArray();
133+
var indexArr = safety.ParamExprMap.ToList()
134+
.Zip(Enumerable.Repeat(0, safety.ParamExprMap.Count), (x, y) => (x.Key, y)).ToArray();
135+
var universe = safety.ParamExprMap.ToDictionary(kv => kv.Key, kv => kv.Value.Count);
136+
var assignmentIndices = new List<Dictionary<string, int>>();
59137
do
60138
{
61139
var indexDic = indexArr.ToDictionary(item => item.Item1, item => item.Item2);
62140
var dic = IndexDic2Dic(globalParams, safety.ParamExprMap, indexDic);
63-
// Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr}");
64-
// Console.WriteLine($"{string.Join(',', dic.ToList())} |- {safety.AssumeExpr} = {ForceBool(Eval(dic, safety.AssumeExpr))}");
65141
if (!SimpleExprEval.ForceBool(SimpleExprEval.Eval(dic, safety.AssumeExpr))) continue;
66-
// Console.WriteLine($"indexArr: {string.Join(',', indexArr)}");
67-
f(dic);
142+
assignmentIndices.Add(indexDic);
68143
} while (Next(indexArr, safety.ParamExprMap));
144+
145+
foreach (var i in GreedyCoverageExplore(universe, assignmentIndices, safety.Twise))
146+
f(IndexDic2Dic(globalParams, safety.ParamExprMap, assignmentIndices[i]));
69147
}
70148
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,25 @@ test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false
2929
assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
3030
(union Client, Bank, { TestWithConfig });
3131

32+
test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false])
33+
assume (b1 == (nClients + g1 > g2))
34+
(4 wise) testTWise4 [main=TestWithConfig]:
35+
assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
36+
(union Client, Bank, { TestWithConfig });
37+
38+
test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false])
39+
assume (b1 == (nClients + g1 > g2))
40+
(3 wise) testTWise3 [main=TestWithConfig]:
41+
assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
42+
(union Client, Bank, { TestWithConfig });
43+
44+
test param (nClients in [2, 3, 4], g1 in [1,2], g2 in [4, 5], b1 in [true, false])
45+
assume (b1 == (nClients + g1 > g2))
46+
(2 wise) testTWise2 [main=TestWithConfig]:
47+
assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in
48+
(union Client, Bank, { TestWithConfig });
49+
50+
3251
// Syntax error
3352
// paramtest () wrong1 [main=TestWithSingleClient]:
3453
// assert BankBalanceIsAlwaysCorrect, GuaranteedWithDrawProgress in

0 commit comments

Comments
 (0)