Dev p3.0/param testcases

.github/workflows/macosci.yml

@@ -24,4 +24,10 @@ jobs:
     - name: Build
       run: dotnet build --configuration Release
     - name: Test
-      run: dotnet test --configuration Release
+      run: dotnet test --configuration Release --blame-crash --blame-hang --blame-hang-timeout 300s --logger:"console;verbosity=detailed"
+    - name: Upload Test Results
+      uses: actions/upload-artifact@v4
+      if: always()  # This ensures it runs even after test failure
+      with:
+        name: test-results
+        path: Tst/UnitTests/TestResults/**/*.xml

Src/PChecker/CheckerCore/Checker.cs

@@ -1,8 +1,8 @@
 using System;
 using PChecker.IO.Debugging;
 using PChecker.IO.Logging;
-using PChecker.SystematicTesting;
 using PChecker.Testing;
+using PChecker.SystematicTesting;
 
 namespace PChecker;
 
@@ -51,7 +51,12 @@ public static void Run(CheckerConfiguration configuration)
             switch (configuration.Mode)
             {
                 case CheckerMode.BugFinding:
-                    TestingProcess.Create(configuration).Run();
+                    var testingEngine = TestingProcess.Create(configuration);
+                    if (configuration.ListTestCases)
+                    {
+                        break;
+                    }
+                    testingEngine.Run();
                     break;
                 case CheckerMode.PEx:
                     ExhaustiveEngine.Create(configuration).Run();

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -176,7 +176,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration) =>
         /// <summary>
         /// Creates a new systematic testing engine.
         /// </summary>
-        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly)
+        private static TestingEngine Create(CheckerConfiguration checkerConfiguration, Assembly assembly)
         {
             if (checkerConfiguration.ListTestCases)
             {
@@ -190,7 +190,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, As
                         Console.Out.WriteLine($"{mi.DeclaringType.Name}");
                     }
 
-                    Environment.Exit(0);
+                    return null;
                 }
                 catch
                 {

Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs

@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using System.ComponentModel.Design;
 using System.IO;
 using System.Linq;
 using System.Reflection;
@@ -21,7 +22,8 @@ public class PCheckerCodeGenerator : ICodeGenerator
         /// This compiler has a compilation stage.
         /// </summary>
         public bool HasCompilationStage => true;
-        private static List<Variable> _globalParams = [];
+        [ThreadStatic]
+        private static List<Variable> _globalParams;
 
         private string GetGlobalParamAndLocalVariableName(CompilationContext context, Variable v)
         {
@@ -346,6 +348,7 @@ private static void WriteForeignType(CompilationContext context, StringWriter ou
         // For normal test, the assignment is empty dictionary
         private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, Dictionary<Variable, IPExpr> assignment)
         {
+            // Console.WriteLine($"dic: {string.Join(',', dic.ToList())}");
             WriteNameSpacePrologue(context, output);
             var name = ParamAssignment.RenameSafetyTestByAssignment(context.Names.GetNameForDecl(safety), assignment);
             context.WriteLine(output, $"public class {name} {{");

Src/PCompiler/CompilerCore/TypeChecker/ParamAssignment.cs

@@ -110,6 +110,11 @@ private static Dictionary<Variable, IPExpr> IndexDic2Dic(List<Variable> globalPa
         foreach (var (k, i) in indexDic)
         {
             var values = paramExprDic[k];
+            if (!globalParams.Any(v => v.Name == k))
+            {
+                throw new Exception($"Variable name '{k}' not found in globalParams. " +
+                                    $"GlobalParams are: [{string.Join(", ", globalParams.Select(v => v.Name))}]");
+            }
             var variable = globalParams.First(v => v.Name == k);
             if (i >= values.Count) throw new ArgumentException("Index out of range in global variable config.");
             dic[variable] = values[i];

Src/PCompiler/CompilerCore/TypeChecker/ParamVisitor.cs

@@ -46,16 +46,25 @@ public override IPExpr VisitSeqLiteralBody([NotNull] PParser.SeqLiteralBodyConte
             if (context.primitive() != null)
             {
                 var values = context.primitive().Select(Visit).ToList();
-                if (values.Count == 0) return new SeqLiteralExpr(context, values, PrimitiveType.Int);
-                // Console.WriteLine($"value[0] = {values[0].GetType()}");
+
+                if (values.Count == 2 &&
+                    values[0] is IntLiteralExpr first &&
+                    values[1] is IntLiteralExpr second &&
+                    first.Value == second.Value)
+                {
+                    throw handler.InternalError(context, new Exception("Invalid range: start and end must not be equal (e.g., [2, 2] is not allowed)"));                }
+
+                if (values.Count == 0)
+                    return new SeqLiteralExpr(context, values, PrimitiveType.Int);
+
                 var type = values[0].Type;
                 foreach (var v in values.Where(v => !v.Type.Equals(type)))
                 {
                     throw handler.TypeMismatch(v.SourceLocation, v.Type, type);
                 }
+
                 return new SeqLiteralExpr(context, values, new SequenceType(type));
-
-            } 
+            }
             if (context.seqLiteral() != null)
             {
                 return Visit(context.seqLiteral());

Src/PCompiler/PCommandLine/CommandLine.cs

@@ -17,7 +17,7 @@ public static class CommandLine
 
         private static readonly object ConsoleLock = new object();
 
-        private static void Main(string[] args)
+        public static void Main(string[] args)
         {
             // Save these so we can force output to happen even if TestingProcess has re-routed it.
             StdOut = Console.Out;

Src/PEx/src/test/java/pex/TestPEx.java

@@ -187,7 +187,11 @@ Collection<DynamicTest> loadTests(String testDirPath) {
             pathKeys.sort(String.CASE_INSENSITIVE_ORDER);
 
             if (testDir.contains("Correct")) {
+
                 for (String key : pathKeys) {
+                    if (key.contains("ParamTest")) {
+                        continue;
+                    }
                     runDynamicTest(0, paths.get(key), key, dynamicTests);
                 }
             } else if (testDir.contains("DynamicError")) {

Tst/CorrectLogs/bugs2/Main_0_0.trace.json → Tst/CorrectLogs/bugs2/bug2_0_0.trace.json

@@ -1,15 +1,4 @@
-[
-  {
-    "type": "CreateStateMachine",
-    "details": {
-      "log": "Main(1) was created by task \u00272\u0027.",
-      "id": "Main(1)",
-      "payload": "null",
-      "clock": {
-        "Main(1)": 1
-      }
-    }
-  },
+ [
   {
     "type": "StateTransition",
     "details": {

Tst/CorrectLogs/bugs2/Main_0_0.txt → Tst/CorrectLogs/bugs2/bug2_0_0.txt

@@ -1,5 +1,3 @@
-<TestLog> Running test 'DefaultImpl'.
-<CreateLog> Main(1) was created by task '2'.
 <StateLog> Main(1) enters state 'S'.
 <RaiseLog> 'Main(1)' raised event 'x with payload (<a,3,>)' in state 'S'.
 <RaiseLog> 'Main(1)' raised event 'a with payload (3)' in state 'S'.

Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ExpectedParametricTests.txt

@@ -0,0 +1,69 @@
+BasicNonParametricTest
+FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_7
+FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_7
+FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_7
+FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_7
+FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_7
+FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_7
+FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_7
+FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_7
+FullCartesianProductParametricTest___g1_1__g2_3__g3_5__g4_8
+FullCartesianProductParametricTest___g1_2__g2_3__g3_5__g4_8
+FullCartesianProductParametricTest___g1_1__g2_4__g3_5__g4_8
+FullCartesianProductParametricTest___g1_2__g2_4__g3_5__g4_8
+FullCartesianProductParametricTest___g1_1__g2_3__g3_6__g4_8
+FullCartesianProductParametricTest___g1_2__g2_3__g3_6__g4_8
+FullCartesianProductParametricTest___g1_1__g2_4__g3_6__g4_8
+FullCartesianProductParametricTest___g1_2__g2_4__g3_6__g4_8
+ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_7
+ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_7
+ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_7
+ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_7
+ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_7
+ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_7
+ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_7
+ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_7
+ParametricTestWithAssumption___g1_1__g2_3__g3_5__g4_8
+ParametricTestWithAssumption___g1_2__g2_3__g3_5__g4_8
+ParametricTestWithAssumption___g1_1__g2_4__g3_5__g4_8
+ParametricTestWithAssumption___g1_2__g2_4__g3_5__g4_8
+ParametricTestWithAssumption___g1_1__g2_3__g3_6__g4_8
+ParametricTestWithAssumption___g1_2__g2_3__g3_6__g4_8
+ParametricTestWithAssumption___g1_1__g2_4__g3_6__g4_8
+ParametricTestWithAssumption___g1_2__g2_4__g3_6__g4_8
+ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_7__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_3__g3_5__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_3__g3_5__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_4__g3_5__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_4__g3_5__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_3__g3_6__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_3__g3_6__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_1__g2_4__g3_6__g4_8__b1_False
+ParametricTestWithBoolAssumption___g1_2__g2_4__g3_6__g4_8__b1_False
+TWise1CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
+TWise1CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False
+TWise2CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
+TWise2CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_True
+TWise2CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False
+TWise2CoverageTest___g1_1__g2_3__g3_6__g4_8__b1_False
+TWise2CoverageTest___g1_2__g2_3__g3_6__g4_7__b1_True
+TWise2CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True
+TWise3CoverageTest___g1_1__g2_3__g3_5__g4_7__b1_True
+TWise3CoverageTest___g1_2__g2_4__g3_6__g4_7__b1_True
+TWise3CoverageTest___g1_2__g2_3__g3_5__g4_8__b1_False
+TWise3CoverageTest___g1_1__g2_4__g3_6__g4_8__b1_False
+TWise3CoverageTest___g1_1__g2_4__g3_5__g4_8__b1_True
+TWise3CoverageTest___g1_2__g2_3__g3_6__g4_8__b1_True
+TWise3CoverageTest___g1_2__g2_4__g3_5__g4_7__b1_False
+TWise3CoverageTest___g1_1__g2_3__g3_6__g4_7__b1_False
+TWise3CoverageTest___g1_2__g2_3__g3_5__g4_7__b1_True
+TWise3CoverageTest___g1_1__g2_4__g3_6__g4_7__b1_True
+TWise3CoverageTest___g1_1__g2_3__g3_5__g4_8__b1_False
+TWise3CoverageTest___g1_2__g2_4__g3_6__g4_8__b1_False

Tst/RegressionTests/Feature1SMLevelDecls/Correct/ParamTest/ParamTest.p

@@ -0,0 +1,33 @@
+param g1 : int;
+param g2 : int;
+param g3 : int;
+param g4 : int;
+
+machine Main {
+	var M: machine;
+	start state Init {
+		entry {
+			print format("global varaible g1 = {0}", g1);
+      print format("global varaible g2 = {0}", g2);
+			print format("global varaible g3 = {0}", g3);
+			print format("global varaible g4 = {0}", g4);
+		}
+	}
+}
+
+
+test BasicNonParametricTest [main=Main]:{Main};
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8]) FullCartesianProductParametricTest [main=Main]:{Main};
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8]) assume (g1 + g2 < g3 + g4) ParametricTestWithAssumption [main=Main]:{Main};
+
+param b1: bool;
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) assume (b1 == (g1 + g2 > g3 + g4)) ParametricTestWithBoolAssumption [main=Main]:{Main};
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (1 wise) TWise1CoverageTest [main=Main]:{Main};
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (2 wise) TWise2CoverageTest [main=Main]:{Main};
+
+test param (g1 in [1, 2], g2 in [3, 4], g3 in [5, 6], g4 in [7, 8], b1 in [true, false]) (3 wise) TWise3CoverageTest [main=Main]:{Main};

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ExpectedParametricTests.txt

@@ -0,0 +1 @@
+TestParam___g1_1__g2_3

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/ParamTest2/ParamTest2.p

@@ -0,0 +1,17 @@
+param g1 : int;
+param g2 : int;
+
+
+machine Main {
+	var M: machine;
+	start state Init {
+		entry {
+			print format("global varaible g1 = {0}", g1);
+      print format("global varaible g2 = {0}", g2);
+			assert g1 != 1 && g2 != 3 ;
+		}
+	}
+}
+
+
+test param (g1 in [1], g2 in [3]) TestParam [main=Main]:{Main};

Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest3/ParamTest3.p

@@ -0,0 +1,13 @@
+param g1 : int;
+
+machine Main {
+	var M: machine;
+	start state Init {
+		entry {
+			print format("global varaible g1 = {0}", g1);
+		}
+	}
+}
+
+test param (g1 in [2, 2]) Test1 [main=Main]:{Main};
+

Tst/RegressionTests/Feature1SMLevelDecls/StaticError/ParamTest4/ParamTest4.p

@@ -0,0 +1,13 @@
+param g1 : int;
+
+machine Main {
+	var M: machine;
+	start state Init {
+		entry {
+			print format("global varaible g1 = {0}", g1);
+		}
+	}
+}
+
+
+test param (g1 in [1, 2]) (0 wise) TWise0CoverageTest [main=Main]:{Main};

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

@@ -37,7 +37,7 @@ fun CreateRandomInitialAccounts(numAccounts: int) : map[int, int]
   var i: int;
   var bankBalance: map[int, int];
   while(i < numAccounts) {
-    bankBalance[i] = choose(10) + 10; // min 10 in the account
+    bankBalance[i] = choose(100) + 10; // min 10 in the account
     i = i + 1;
   }
   return bankBalance;

Tst/UnitTests/PCheckerLogGeneratorTests.cs

@@ -26,10 +26,10 @@ public void TestLogGenerator()
         var tempDir = Directory.CreateDirectory(testLogGeneratorPath);
         var srcPath = new FileInfo(Path.Combine(Constants.SolutionDirectory, "Tst", "RegressionTests",
             "Feature1SMLevelDecls", "DynamicError", "bug2", "bug2.p"));
-        var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "PChecker", "net8.0", "Main.dll");
+        var runner = new PCheckerRunner([srcPath]);
+        var dllPath = Path.Combine(Constants.ScratchParentDirectory, "TestLogGenerator", "PChecker", "net8.0", "bug2.dll");
         var expectedPath = Path.Combine(Constants.SolutionDirectory, "Tst", "CorrectLogs", "bugs2");
 
-        var runner = new PCheckerRunner([srcPath]);
         runner.DoCompile(tempDir);
 
         var configuration = new PCheckerOptions().Parse([dllPath, "-o", tempDir.ToString()]);
@@ -53,14 +53,25 @@ private void AssertLog(string generatedDir, string expectedDir)
             string generatedFilePath = Path.Combine(generatedDir, fileName);
             string expectedFilePath = Path.Combine(expectedDir, fileName);
 
-            if (fileName == "Main_0_0.trace.json")
+            if (fileName == "bug2_0_0.trace.json")
             {
                 // Perform "Is JSON Included" check for this specific file
                 if (!IsJsonContentIncluded(generatedFilePath, expectedFilePath))
                 {
                     Assert.Fail($"Test Failed \nContent of {expectedFilePath} is not fully included in {generatedFilePath}");
                 }
             }
+            else if (fileName == "bug2_0_0.txt")
+            {
+                // Perform "Is text included" check for this specific file
+                var expectedContent = File.ReadAllText(expectedFilePath);
+                var generatedContent = File.ReadAllText(generatedFilePath);
+
+                if (!generatedContent.Contains(expectedContent))
+                {
+                    Assert.Fail($"Test Failed \nExpected content from {expectedFilePath} not found in {generatedFilePath}");
+                }
+            }
             else
             {
                 // Perform exact match for other files
@@ -128,4 +139,4 @@ private static bool IsSubset(JToken subset, JToken superset)
 
         return false;
     }
-}
+}