Param

.github/workflows/macosci.yml

@@ -16,7 +16,7 @@ jobs:
       with:
         java-version: 11
     - name: Cache Maven packages
-      uses: actions/cache@v2
+      uses: actions/cache@v3
       with:
         path: ~/.m2
         key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}

.github/workflows/ubuntuci.yml

@@ -16,7 +16,7 @@ jobs:
       with:
         java-version: 11
     - name: Cache Maven packages
-      uses: actions/cache@v2
+      uses: actions/cache@v3
       with:
         path: ~/.m2
         key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}

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,11 +22,11 @@ public class PCheckerCodeGenerator : ICodeGenerator
         /// This compiler has a compilation stage.
         /// </summary>
         public bool HasCompilationStage => true;
-        private List<Variable> _globalVariables = [];
+        private static List<Variable> _globalParams = [];
 
-        private string GetGlobalAndLocalVariableName(CompilationContext context, Variable v)
+        private string GetGlobalParamAndLocalVariableName(CompilationContext context, Variable v)
         {
-            return _globalVariables.Contains(v) ? $"({ICodeGenerator.GlobalConfigName}.{v.Name})" : context.Names.GetNameForDecl(v);
+            return _globalParams.Contains(v) ? $"({ICodeGenerator.GlobalConfigName}.{v.Name})" : context.Names.GetNameForDecl(v);
         }
 
         public void Compile(ICompilerConfiguration job)
@@ -97,9 +98,9 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop
 
             WriteSourcePrologue(context, source.Stream);
 
-            _globalVariables = globalScope.GetGlobalVariables();
+            _globalParams = globalScope.GetGlobalVariables();
 
-            DeclareGlobalConstantVariables(context, source.Stream);
+            DeclareGlobalParams(context, source.Stream);
 
             // write the top level declarations
             foreach (var decl in globalScope.AllDecls)
@@ -254,7 +255,8 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
                     break;
 
                 case SafetyTest safety:
-                    WriteSafetyTestDecl(context, output, safety);
+                    ParamAssignment.IterateAssignments(safety, _globalParams, 
+                        assignment => WriteSafetyTestDecl(context, output, safety, assignment));
                     break;
 
                 case Interface _:
@@ -273,14 +275,14 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
             }
         }
 
-        private void DeclareGlobalConstantVariables(CompilationContext context, StringWriter output)
+        private void DeclareGlobalParams(CompilationContext context, StringWriter output)
         {
             WriteNameSpacePrologue(context, output);
             context.WriteLine(output, $"public static class {ICodeGenerator.GlobalConfigName}");
             context.WriteLine(output, "{");
-            foreach (var v in _globalVariables)
+            foreach (var v in _globalParams)
             {
-                if (v.Role != VariableRole.GlobalConstant)
+                if (v.Role != VariableRole.GlobalParams)
                 {
                     throw context.Handler.InternalError(v.SourceLocation, new ArgumentException("The role of global variable is not global."));
                 }
@@ -343,31 +345,15 @@ private static void WriteForeignType(CompilationContext context, StringWriter ou
             var declName = foreignType.CanonicalRepresentation;
             context.WriteLine(output, $"// TODO: Implement the Foreign Type {declName}");
         }
-
-        private static string RenameSafetyTest(string name, IDictionary<string, int> indexDic)
-        {
-            var postfix = $"{string.Join('_', indexDic.ToList().Select(p => $"{p.Key}_{p.Value}"))}";
-            return postfix.Length == 0 ? name : $"{name}__{postfix}";
-        }
 
-        private void WriteSingleSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, IDictionary<string, int> indexDic)
+        // For normal test, the assignment is empty dictionary
+        private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety, Dictionary<Variable, IPExpr> assignment)
         {
-            // Console.WriteLine($"indexArr: {string.Join(',', indexDic.ToList())}");
+            // Console.WriteLine($"dic: {string.Join(',', dic.ToList())}");
             WriteNameSpacePrologue(context, output);
-            var name = RenameSafetyTest(context.Names.GetNameForDecl(safety), indexDic);
+            var name = ParamAssignment.RenameSafetyTestByAssignment(context.Names.GetNameForDecl(safety), assignment);
             context.WriteLine(output, $"public class {name} {{");
-            var dic = new Dictionary<Variable, IPExpr>();
-            foreach (var (k, i) in indexDic)
-            {
-                var values = safety.ParamExpr[k];
-                var variable = _globalVariables.First(v => v.Name == k);
-                if (i >= values.Count)
-                {
-                    throw context.Handler.InternalError(variable.SourceLocation, new ArgumentException("Index out of range in global variable config.")); 
-                }
-                dic[variable] = values[i];
-            }
-            WriteInitializeGlobalConstantVariables(context, output, dic);
+            WriteInitializeGlobalParams(context, output, assignment);
             WriteInitializeLinkMap(context, output, safety.ModExpr.ModuleInfo.LinkMap);
             WriteInitializeInterfaceDefMap(context, output, safety.ModExpr.ModuleInfo.InterfaceDef);
             WriteInitializeMonitorObserves(context, output, safety.ModExpr.ModuleInfo.MonitorMap.Keys);
@@ -377,43 +363,6 @@ private void WriteSingleSafetyTestDecl(CompilationContext context, StringWriter
 
             WriteNameSpaceEpilogue(context, output);
         }
-
-        private bool Next((string, int)[] indexArr, IDictionary<string, List<IPExpr>> globalConstants)
-        {
-            for (var i = 0; i < indexArr.Length; i++)
-            {
-                indexArr[i] = (indexArr[i].Item1, indexArr[i].Item2 + 1);
-                // Console.WriteLine($"globalConstants[globalVariables[{i}].Name].Count = {globalConstants[globalVariables[i].Name].Count}");
-                if (indexArr[i].Item2 < globalConstants[indexArr[i].Item1].Count) return true;
-                indexArr[i] = (indexArr[i].Item1, 0);
-            }
-            return false;
-        }
-
-        private void WriteSafetyTestDecl(CompilationContext context, StringWriter output, SafetyTest safety)
-        {
-            if (safety.ParamExpr.Count == 0)
-            {
-                WriteSingleSafetyTestDecl(context, output, safety, new Dictionary<string, int>());
-                return;
-            }
-            var globalConstants = safety.ParamExpr;
-            // Console.WriteLine($"safety.ParamExpr.Count = {safety.ParamExpr.Count}");
-            var indexArr = globalConstants.ToList().Zip(Enumerable.Repeat(0, safety.ParamExpr.Count), (x, y) => (x.Key, y)).ToArray();
-            // Console.WriteLine($"global: {string.Join(',', globalConstants.Values.Select(x => x.Count))}");
-            // Console.WriteLine($"indexArr: {string.Join(',', indexArr)}");
-
-            do
-            {
-                var indexDic = new Dictionary<string, int>();
-                for (var i = 0; i < indexArr.Length; i++)
-                {
-                    indexDic[indexArr[i].Item1] = indexArr[i].Item2;
-                }
-
-                WriteSingleSafetyTestDecl(context, output, safety, indexDic);
-            } while (Next(indexArr, globalConstants));
-        }
 
         private void WriteImplementationDecl(CompilationContext context, StringWriter output, Implementation impl)
         {
@@ -472,27 +421,27 @@ private void WriteInitializeEnums(CompilationContext context, StringWriter outpu
             WriteNameSpaceEpilogue(context, output);
         }
 
-        private const string InitGlobalConstantsVariablesFunctionName = "InitializeGlobalConstantVariables";
+        private const string InitGlobalParamsFunctionName = "InitializeGlobalParams";
 
-        private void WriteInitializeGlobalConstantVariables(CompilationContext context, StringWriter output, IDictionary<Variable, IPExpr> dic)
+        private void WriteInitializeGlobalParams(CompilationContext context, StringWriter output, IDictionary<Variable, IPExpr> dic)
         {
-            context.WriteLine(output, $"public static void {InitGlobalConstantsVariablesFunctionName}() {{");
+            context.WriteLine(output, $"public static void {InitGlobalParamsFunctionName}() {{");
             foreach (var (v, value) in dic)
             {
-                var varName = GetGlobalAndLocalVariableName(context, v);
+                var varName = GetGlobalParamAndLocalVariableName(context, v);
                 context.Write(output, $"  {varName} = ");
                 WriteExpr(context, output, value);
                 context.WriteLine(output, $";");
             }
             context.WriteLine(output, "}");
         }
 
-        private void WriteTestFunction(CompilationContext context, StringWriter output, string main, bool ifInitGlobalVars)
+        private void WriteTestFunction(CompilationContext context, StringWriter output, string main, bool ifInitGlobalParams)
         {
             context.WriteLine(output);
             context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
             context.WriteLine(output, "public static void Execute(ControlledRuntime runtime) {");
-            if (ifInitGlobalVars) { context.WriteLine(output, $"{InitGlobalConstantsVariablesFunctionName}();"); }
+            if (ifInitGlobalParams) { context.WriteLine(output, $"{InitGlobalParamsFunctionName}();"); }
             context.WriteLine(output, "PModule.runtime = runtime;");
             context.WriteLine(output, "PHelper.InitializeInterfaces();");
             context.WriteLine(output, "PHelper.InitializeEnums();");
@@ -1280,7 +1229,7 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr
                     break;
 
                 case VariableAccessExpr variableAccessExpr:
-                    var varName = GetGlobalAndLocalVariableName(context, variableAccessExpr.Variable);
+                    var varName = GetGlobalParamAndLocalVariableName(context, variableAccessExpr.Variable);
                     context.Write(output, varName);
                     break;
 
@@ -1621,7 +1570,7 @@ private void WriteClone(CompilationContext context, StringWriter output, IExprTe
                 return;
             }
 
-            var varName = GetGlobalAndLocalVariableName(context, variableRef.Variable);
+            var varName = GetGlobalParamAndLocalVariableName(context, variableRef.Variable);
             context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPValue){varName})?.Clone())");
         }
 

Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

@@ -53,22 +53,22 @@ public Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplica
                 $"'{duplicate.Name}' duplicates declaration '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
-        public Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
+        public Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
         {
             return IssueError(location,
-                $"'{duplicate.Name}' redeclares a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+                $"'{duplicate.Name}' redeclares a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
-        public Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name)
+        public Exception UndeclaredGlobalParam(ParserRuleContext location, string name)
         {
             return IssueError(location,
-                $"'global constant variable {name}' is not undeclared");
+                $"'global param {name}' is not undeclared");
         }
 
-        public Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing)
+        public Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing)
         {
             return IssueError(location,
-                $"try to modify a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+                $"try to modify a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
         public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)

Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

@@ -24,11 +24,11 @@ Exception DuplicateStartState(
 
         Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
 
-        Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
+        Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
 
-        Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name);
+        Exception UndeclaredGlobalParam(ParserRuleContext location, string name);
 
-        Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing);
+        Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
 
         Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
 

Src/PCompiler/CompilerCore/Parser/PLexer.g4

@@ -59,7 +59,7 @@ THIS      : 'this' ;
 TYPE      : 'type' ;
 VALUES    : 'values' ;
 VAR       : 'var' ;
-CONSTANT       : 'constant' ;
+PARAM       : 'param' ;
 WHILE     : 'while' ;
 WITH      : 'with' ;
 CHOOSE    : 'choose' ;

Src/PCompiler/CompilerCore/Parser/PParser.g4

@@ -60,10 +60,10 @@ topDecl : typeDefDecl
         | namedModuleDecl
         | testDecl
         | implementationDecl
-        | globalValDecl
+        | globalParamDecl
         ;
 
-globalValDecl : CONSTANT idenList COLON type SEMI ;
+globalParamDecl : PARAM idenList COLON type SEMI ;
 
 typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef
             | TYPE name=iden ASSIGN type SEMI # PTypeDef
@@ -253,8 +253,7 @@ paramBody : name=iden IN value=seqLiteral
           ;
 param : LPAREN paramBody RPAREN;
 
-testDecl : TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI                  # SafetyTestDecl
-         | PARAMTEST globalParam=param testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # ParametricSafetyTestDecl
+testDecl : TEST (PARAM globalParam=param)? (ASSUME assumeExpr=expr)? 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/Function.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
-using System.Linq;
 using Antlr4.Runtime;
 using Plang.Compiler.TypeChecker.AST.Statements;
 
@@ -23,7 +22,6 @@ public class Function : IPDecl, IHasScope
     {
         private readonly HashSet<Function> callees = new HashSet<Function>();
         private readonly HashSet<Function> callers = new HashSet<Function>();
-        private readonly List<Variable> _globalConstantVariables = [];
         private readonly List<Variable> localVariables = new List<Variable>();
         private readonly List<Interface> createsInterfaces = new List<Interface>();
 
@@ -67,24 +65,6 @@ public Function(ParserRuleContext sourceNode) : this("", sourceNode)
 
         public string Name { get; set; }
         public ParserRuleContext SourceLocation { get; }
-
-        public void AddGlobalConstantVariables(ITranslationErrorHandler handler, List<Variable> gvars)
-        {
-            var localNames = localVariables.Select(x => x.Name);
-            // Console.WriteLine("localNames:" + localNames.ToArray());
-            foreach (var g in gvars)
-            {
-                var res = localVariables.Find(x => x.Name == g.Name);
-                if (res == null)
-                {
-                    _globalConstantVariables.Add(g);
-                }
-                else
-                {
-                    throw handler.RedeclareGlobalConstantVariable(res.SourceLocation, res, g);
-                }
-            }
-        }
 
         public void AddLocalVariable(Variable local)
         {

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

@@ -1,21 +1,21 @@
 using Antlr4.Runtime;
 using System.Collections.Generic;
+using Plang.Compiler.TypeChecker.AST.Expressions;
 
 namespace Plang.Compiler.TypeChecker.AST.Declarations
 {
-    public class SafetyTest : IPDecl
+    public class SafetyTest(ParserRuleContext sourceNode, string testName) : IPDecl
     {
-        public SafetyTest(ParserRuleContext sourceNode, string testName)
-        {
-            SourceLocation = sourceNode;
-            Name = testName;
-        }
-
         public string Main { get; set; }
         public IPModuleExpr ModExpr { get; set; }
-
-        public IDictionary<string, List<IPExpr>> ParamExpr { get; set; }
-        public string Name { get; }
-        public ParserRuleContext SourceLocation { get; }
+
+        // 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>>();
+
+        // By default, assumption expression is true
+        public IPExpr AssumeExpr { get; set; } = new BoolLiteralExpr(true);
+
+        public string Name { get; } = testName;
+        public ParserRuleContext SourceLocation { get; } = sourceNode;
     }
 }

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

@@ -18,6 +18,11 @@ public Variable(string name, ParserRuleContext sourceNode, VariableRole role)
 
         public string Name { get; }
         public ParserRuleContext SourceLocation { get; }
+
+        public override string ToString()
+        {
+            return this.Name;
+        }
     }
 
     [Flags]
@@ -27,6 +32,6 @@ public enum VariableRole
         Param = 1 << 1,
         Field = 1 << 2,
         Temp = 1 << 3,
-        GlobalConstant = 1 << 4
+        GlobalParams = 1 << 4
     }
 }