knocking out edge cases with ors, xors, ands in statecharts

Fault-lang · Jan 16, 2023 · e52f332 · e52f332
1 parent c416a46
commit e52f332
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 11 deletions.
diff --git a/llvm/compiler.go b/llvm/compiler.go
@@ -136,9 +136,22 @@ func (c *Compiler) processSpec(root ast.Node, isImport bool) ([]*ast.AssertionSt
 		c.currentSpec = decl.Name.Value
 	case *ast.SysDeclStatement:
 		for _, v := range specfile.Statements {
-			if _, ok := v.(*ast.ForStatement); ok {
+			switch n := v.(type) {
+			case *ast.ForStatement:
 				c.hasRunBlock = true
 				continue
+			case *ast.DefStatement:
+				if cm, ok := n.Value.(*ast.ComponentLiteral); ok {
+					//assembling component parts as params
+					id := cm.Id()
+					s := c.specStructs[id[0]]
+					branches, err := s.FetchComponent(id[1])
+					if err != nil {
+						panic(err)
+					}
+					params := c.generateParameters(cm.Id(), branches, true)
+					c.sysGlobals = append(c.sysGlobals, params...)
+				}
 			}
 		}
 		c.currentSpec = decl.Name.Value
@@ -411,7 +424,7 @@ func (c *Compiler) compileComponent(node *ast.ComponentLiteral) {
 			parentID := node.IdString()
 			c.structPropOrder[childId] = c.structPropOrder[parentID]
 
-			params := c.generateParameters(id, tree, true)
+			params := []*ir.Param{}
 			params = c.includeGlobalParams(params)
 			s := c.specs[id[0]]
 			funcId := append(p.(ast.Nameable).Id(), "__state")

diff --git a/smt/rules_types.go b/smt/rules_types.go
@@ -364,27 +364,51 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
 }
 
 func (g *Generator) xorRule(inst *ir.InstXor) rule {
+	id := inst.Ident()
 	x := inst.X.Ident()
-	x = g.variables.convertIdent(g.currentFunction, x)
-	return g.parseRule(x, "", "", "not")
+	xRule := g.variables.lookupCondPart(g.currentFunction, x)
+	if xRule == nil {
+		x = g.variables.convertIdent(g.currentFunction, x)
+		xRule = &wrap{value: x}
+	}
+	return g.parseMultiCond(id, xRule, &wrap{}, "not")
 }
 
 func (g *Generator) andRule(inst *ir.InstAnd) rule {
 	id := inst.Ident()
 	x := inst.X.Ident()
 	y := inst.Y.Ident()
+
 	xRule := g.variables.lookupCondPart(g.currentFunction, x)
+	if xRule == nil {
+		x = g.variables.convertIdent(g.currentFunction, x)
+		xRule = &wrap{value: x}
+	}
+
 	yRule := g.variables.lookupCondPart(g.currentFunction, y)
+	if yRule == nil {
+		y = g.variables.convertIdent(g.currentFunction, y)
+		yRule = &wrap{value: y}
+	}
 	return g.parseMultiCond(id, xRule, yRule, "and")
 }
 
 func (g *Generator) orRule(inst *ir.InstOr) rule {
 	x := inst.X.Ident()
 	y := inst.Y.Ident()
 	id := inst.Ident()
-	x = g.variables.convertIdent(g.currentFunction, x)
-	y = g.variables.convertIdent(g.currentFunction, y)
-	return g.parseInfix(id, x, y, "or")
+	xRule := g.variables.lookupCondPart(g.currentFunction, x)
+	if xRule == nil {
+		x = g.variables.convertIdent(g.currentFunction, x)
+		xRule = &wrap{value: x}
+	}
+
+	yRule := g.variables.lookupCondPart(g.currentFunction, y)
+	if yRule == nil {
+		y = g.variables.convertIdent(g.currentFunction, y)
+		yRule = &wrap{value: y}
+	}
+	return g.parseMultiCond(id, xRule, yRule, "or")
 }
 
 func (g *Generator) stateRules(key string, sc *stateChange) rule {

diff --git a/smt/variables_writer.go b/smt/variables_writer.go
@@ -197,12 +197,9 @@ func (g *variables) lookupCondPart(f string, val string) rule {
 		refname := fmt.Sprintf("%s-%s", f, val)
 		if v, ok := g.ref[refname]; ok {
 			return v
-		} else {
-			panic(fmt.Sprintf("variable %s not initialized", val))
 		}
-	} else {
-		panic(fmt.Sprintf("variable %s not valid construction", val))
 	}
+	return nil
 }
 
 func (g *variables) formatValue(val value.Value) string {