sloppy commit, but when starting state chart temporals I decided to c…

…hange the approach to handling rounds

ast/ast.go

@@ -921,10 +921,8 @@ func (pe *PrefixExpression) Position() []int      { return pe.Token.GetPosition(
 func (pe *PrefixExpression) String() string {
 	var out bytes.Buffer
 
-	out.WriteString("(")
 	out.WriteString(pe.Operator)
 	out.WriteString(pe.Right.String())
-	out.WriteString(")")
 
 	return out.String()
 }

ast/ast_test.go

@@ -160,7 +160,7 @@ func TestString(t *testing.T) {
 			want = "Mean: 2.000000Sigma: 0.400000;"
 		case *PrefixExpression:
 			got = t.String()
-			want = "(!3)"
+			want = "!3"
 		case *InfixExpression:
 			got = t.String()
 			want = "(3 > 3)"
@@ -181,7 +181,7 @@ func TestString(t *testing.T) {
 			want = "test fuzz = 24;"
 		case *ExpressionStatement:
 			got = t.String()
-			want = "(!3)"
+			want = "!3"
 		case *ParallelFunctions:
 			got = t.String()
 			want = "testtest"

grammar/FaultLexer.g4

@@ -31,6 +31,7 @@ RUN: 'run';
 SPEC: 'spec';
 STOCK: 'stock';
 THEN: 'then';
+WHEN: 'when';
 THIS: 'this';
 EVENTUALLY: 'eventually';
 EVENTUALLYALWAYS: 'eventually-always';

grammar/FaultParser.g4

@@ -182,11 +182,11 @@ assumption
 temporal
     : ('eventually' | 'always' | 'eventually-always' )
     | ('nmt' | 'nft') integer
-    | 'then' expression
     ;
 
 invariant
-    : expression
+    : expression                            # invar
+    | 'when' expression 'then' expression   # stageInvariant
     ;
 
 assignment

listener/listener.go

@@ -1239,24 +1239,31 @@ func (l *FaultListener) ExitForStmt(c *parser.ForStmtContext) {
 	}
 }
 
+func (l *FaultListener) ExitStageInvariant(c *parser.StageInvariantContext) {
+	right := l.pop()
+	left := l.pop()
+	token := util.GenerateToken("ASSERT", "assert", c.GetStart(), c.GetStop())
+	l.push(&ast.InvariantClause{
+		Token:    token,
+		Left:     left.(ast.Expression),
+		Operator: "then",
+		Right:    right.(ast.Expression),
+	})
+}
+
 func (l *FaultListener) ExitAssertion(c *parser.AssertionContext) {
 	token := util.GenerateToken("ASSERT", "assert", c.GetStart(), c.GetStop())
 
 	var temporal string
 	var temporalFilter string
 	var temporalN int
-	var err error
 	if c.Temporal() != nil {
 		if c.Temporal().GetChildCount() == 2 {
-			l.pop() // Discard the int
+			i := l.pop()
 			temporalRaw := c.Temporal().GetText()
 			temporal = ""
-			temporalFilter = temporalRaw[0 : len(temporalRaw)-1]
-			temporalN, err = strconv.Atoi(string(temporalRaw[len(temporalRaw)-1]))
-			if err != nil {
-				pos := token.Position
-				panic(fmt.Sprintf("temporal logic not value, filter should be an int: line %d col %d", pos[0], pos[1]))
-			}
+			temporalFilter = temporalRaw[0 : len(temporalRaw)-len(i.(*ast.IntegerLiteral).String())]
+			temporalN = int(i.(*ast.IntegerLiteral).Value)
 		} else {
 			temporal = c.Temporal().GetText()
 		}
@@ -1277,6 +1284,8 @@ func (l *FaultListener) ExitAssertion(c *parser.AssertionContext) {
 			Operator: e.Operator,
 			Right:    e.Right,
 		}
+	case *ast.InvariantClause:
+		con = e
 	}
 
 	l.push(&ast.AssertionStatement{
@@ -1293,18 +1302,13 @@ func (l *FaultListener) ExitAssumption(c *parser.AssumptionContext) {
 	var temporal string
 	var temporalFilter string
 	var temporalN int
-	var err error
 	if c.Temporal() != nil {
 		if c.Temporal().GetChildCount() == 2 {
-			l.pop() // Discard the int
+			i := l.pop()
 			temporalRaw := c.Temporal().GetText()
 			temporal = ""
-			temporalFilter = temporalRaw[0 : len(temporalRaw)-1]
-			temporalN, err = strconv.Atoi(string(temporalRaw[len(temporalRaw)-1]))
-			if err != nil {
-				pos := token.Position
-				panic(fmt.Sprintf("temporal logic not value, filter should be an int: line %d col %d", pos[0], pos[1]))
-			}
+			temporalFilter = temporalRaw[0 : len(temporalRaw)-len(i.(*ast.IntegerLiteral).String())]
+			temporalN = int(i.(*ast.IntegerLiteral).Value)
 		} else {
 			temporal = c.Temporal().GetText()
 		}
@@ -1323,6 +1327,8 @@ func (l *FaultListener) ExitAssumption(c *parser.AssumptionContext) {
 			Operator: e.Operator,
 			Right:    e.Right,
 		}
+	case *ast.InvariantClause:
+		con = e
 	}
 
 	l.push(&ast.AssumptionStatement{

llvm/compiler.go

@@ -22,19 +22,22 @@ var DoubleP = &irtypes.PointerType{ElemType: irtypes.Double}
 var I1P = &irtypes.PointerType{ElemType: irtypes.I1}
 
 var OP_NEGATE = map[string]string{
-	"==": "!=",
-	">=": "<",
-	">":  "<=",
-	"<=": ">",
-	"!=": "==",
-	"<":  ">=",
-	"&&": "||",
-	"||": "&&",
+	"==":   "!=",
+	">=":   "<",
+	">":    "<=",
+	"<=":   ">",
+	"!=":   "==",
+	"<":    ">=",
+	"&&":   "||",
+	"||":   "&&",
+	"then": "then",
 	//"=": "!=",
 }
 
 type Compiler struct {
-	module *ir.Module
+	module  *ir.Module
+	markers []*ir.Global // 0-index -> Round
+	// 1-index -> Parallel Group
 
 	hasRunBlock bool
 	runRound    int16
@@ -94,7 +97,7 @@ func NewCompiler() *Compiler {
 		Uncertains:    make(map[string][]float64),
 		Components:    make(map[string]*StateFunc),
 	}
-	c.addGlobal()
+	c.setup()
 	return c
 }
 
@@ -211,6 +214,7 @@ func (c *Compiler) compile(node ast.Node) {
 	case *ast.ForStatement:
 		c.contextFuncName = "__run"
 		for i := int64(0); i < v.Rounds.Value; i++ {
+			c.contextBlock.NewStore(constant.NewInt(irtypes.I16, int64(c.runRound)), c.markers[0])
 			c.compileBlock(v.Body)
 			c.runRound = c.runRound + 1
 			c.stateCheck()
@@ -1567,7 +1571,12 @@ func (c *Compiler) GetIR() string {
 	return c.module.String()
 }
 
-func (c *Compiler) addGlobal() {
+func (c *Compiler) setup() {
+	//Initialize Markers
+	c.markers = []*ir.Global{
+		c.module.NewGlobalDef("__rounds", constant.NewInt(irtypes.I16, 0)),
+		c.module.NewGlobalDef("__parallelGroup", constant.NewCharArrayFromString("start")),
+	}
 	// run block
 	c.contextFunc = c.module.NewFunc("__run", irtypes.Void)
 	mainBlock := c.contextFunc.NewBlock(name.Block())