moving variable data over to own package and starting generator

execute/execute.go

@@ -5,6 +5,7 @@ import (
 	"errors"
 	"fault/execute/parser"
 	"fault/smt"
+	"fault/smt/variables"
 	"fault/util"
 	"fmt"
 	"os"
@@ -28,7 +29,7 @@ type ModelChecker struct {
 	SMT          string
 	Uncertains   map[string][]float64
 	Unknowns     []string
-	Results      map[string][]*smt.VarChange
+	Results      map[string][]*variables.VarChange
 	ResultValues map[string]string
 	solver       map[string]*Solver
 	forks        map[string][]*Branch
@@ -65,7 +66,7 @@ func GenerateSolver() map[string]*Solver {
 	return s
 }
 
-func (mc *ModelChecker) LoadModel(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) {
+func (mc *ModelChecker) LoadModel(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*variables.VarChange) {
 	mc.SMT = smt
 	mc.Uncertains = uncertains
 	mc.Unknowns = unknowns

execute/execute_test.go

@@ -1,7 +1,7 @@
 package execute
 
 import (
-	"fault/smt"
+	"fault/smt/variables"
 	"testing"
 )
 
@@ -12,7 +12,7 @@ func TestSMTOk(t *testing.T) {
 	(assert (= imports_fl3_vault_value_1 (+ imports_fl3_vault_value_0 10.0)))
 	(assert (= imports_fl3_vault_value_2 (+ imports_fl3_vault_value_1 10.0)))
 	`
-	model := prepTest(test, make(map[string][]float64), []string{}, map[string][]*smt.VarChange{})
+	model := prepTest(test, make(map[string][]float64), []string{}, map[string][]*variables.VarChange{})
 
 	response, err := model.Check()
 
@@ -51,7 +51,7 @@ func TestProbability(t *testing.T) {
 	uncertains := make(map[string][]float64)
 	uncertains["imports_fl3_vault_value"] = []float64{30.0, 5}
 
-	model := prepTest(test, uncertains, []string{}, map[string][]*smt.VarChange{})
+	model := prepTest(test, uncertains, []string{}, map[string][]*variables.VarChange{})
 
 	model.Check()
 	solution, _ := model.Solve()
@@ -64,7 +64,7 @@ func TestProbability(t *testing.T) {
 
 }
 
-func prepTest(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) *ModelChecker {
+func prepTest(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*variables.VarChange) *ModelChecker {
 	ex := NewModelChecker()
 	ex.LoadModel(smt, uncertains, unknowns, results)
 	return ex

execute/format.go

@@ -2,7 +2,7 @@ package execute
 
 import (
 	"bytes"
-	"fault/smt"
+	"fault/smt/variables"
 	"fmt"
 	"strings"
 )
@@ -24,7 +24,7 @@ func (mc *ModelChecker) Mermaid() {
 	}
 }
 
-func (mc *ModelChecker) writeObjects(k string, objects []*smt.VarChange) string {
+func (mc *ModelChecker) writeObjects(k string, objects []*variables.VarChange) string {
 	var objs []string
 	for _, o := range objects {
 		if o.Parent != "" {
@@ -38,7 +38,7 @@ func (mc *ModelChecker) writeObjects(k string, objects []*smt.VarChange) string
 	return strings.Join(objs, "\n")
 }
 
-func (mc *ModelChecker) writeObject(o *smt.VarChange) string {
+func (mc *ModelChecker) writeObject(o *variables.VarChange) string {
 	value, ok := mc.ResultValues[o.Parent]
 	if ok {
 		return fmt.Sprintf("\t% s--> |%s| %s", o.Parent, value, o.Id)

main.go

@@ -9,6 +9,7 @@ import (
 	"fault/preprocess"
 	"fault/reachability"
 	"fault/smt"
+	smtvar "fault/smt/variables"
 	"fault/types"
 	"fault/util"
 	"fault/visualize"
@@ -89,7 +90,7 @@ func smt2(ir string, runs int16, uncertains map[string][]float64, unknowns []str
 	return generator
 }
 
-func probability(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) (*execute.ModelChecker, map[string]execute.Scenario) {
+func probability(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smtvar.VarChange) (*execute.ModelChecker, map[string]execute.Scenario) {
 	ex := execute.NewModelChecker()
 	ex.LoadModel(smt, uncertains, unknowns, results)
 	ok, err := ex.Check()
@@ -183,7 +184,7 @@ func run(filepath string, mode string, input string, reach bool) {
 			mc.Format(data)
 		}
 	case "smt2":
-		mc, data := probability(d, uncertains, unknowns, make(map[string][]*smt.VarChange))
+		mc, data := probability(d, uncertains, unknowns, make(map[string][]*smtvar.VarChange))
 
 		if mode == "visualize" {
 			mc.Mermaid()

smt/asserts.go

@@ -757,7 +757,7 @@ func (g *Generator) wrapPerm(w *rules.Wrap) []string {
 	}
 	if w.All {
 		var states []string
-		end := g.variables.ssa[w.Value]
+		end := g.variables.SSA[w.Value]
 		for i := 0; i < int(end+1); i++ {
 			if !g.filterOutTempStates(w.Value, int16(i)) {
 				states = append(states, fmt.Sprint(w.Value, "_", i))

smt/forks_writer.go

@@ -101,7 +101,7 @@ func (g *Generator) buildForkChoice(rules []rules.Rule, b string) {
 
 	seenVar := make(map[string]bool)
 	for _, s := range stateChanges {
-		base, i := g.variables.getVarBase(s)
+		base, i := g.variables.GetVarBase(s)
 		n := int16(i)
 		// Have we seen this variable in a previous branch of
 		// this fork?
@@ -146,7 +146,7 @@ func (g *Generator) allStateChangesInRule(ru rules.Rule) []string {
 			wg = append(wg, ch...)
 		}
 	case *rules.Wrap:
-		if !g.variables.isNumeric(r.Value) && !g.variables.isBolean(r.Value) { // Wraps might be static values
+		if !g.variables.IsNumeric(r.Value) && !g.variables.IsBoolean(r.Value) { // Wraps might be static values
 			return []string{r.Value}
 		}
 	case *rules.Ands:
@@ -193,7 +193,7 @@ func (g *Generator) runParallel(perm [][]string) []rules.Rule {
 	for i, calls := range perm {
 		branchBlock := fmt.Sprint("option_", i)
 		var opts [][]rules.Rule
-		varState := g.variables.saveState()
+		varState := g.variables.SaveState()
 		for _, c := range calls {
 			g.parallelRunStart = true
 			g.inPhiState.Out() //Don't behave like we're in Phi inside the function
@@ -208,7 +208,7 @@ func (g *Generator) runParallel(perm [][]string) []rules.Rule {
 		// Pull all the variables out of the rules and
 		// sort them into fork choices
 		g.buildForkChoice(raw, "")
-		g.variables.loadState(varState)
+		g.variables.LoadState(varState)
 		ru = append(ru, raw...)
 	}
 
@@ -267,8 +267,8 @@ func (g *Generator) capParallel() []rules.Rule {
 	fork := g.getCurrentFork()
 	var ru []rules.Rule
 	for k, v := range fork {
-		id := g.variables.advanceSSA(k)
-		g.addVarToRound(k, int(g.variables.ssa[k]))
+		id := g.variables.AdvanceSSA(k)
+		g.addVarToRound(k, int(g.variables.SSA[k]))
 
 		var nums []int16
 		for _, c := range v {
@@ -283,12 +283,12 @@ func (g *Generator) capParallel() []rules.Rule {
 		g.VarChangePhi(k, id, nums)
 		ru = append(ru, rule)
 
-		base, i := g.variables.getVarBase(id)
+		base, i := g.variables.GetVarBase(id)
 		n := int16(i)
 		if g.inPhiState.Level() == 1 {
-			g.variables.newPhi(base, n)
+			g.variables.NewPhi(base, n)
 		} else {
-			g.variables.storeLastState(base, n)
+			g.variables.StoreLastState(base, n)
 		}
 
 	}
@@ -300,7 +300,7 @@ func (g *Generator) capRule(k string, nums []int16, id string) []rules.Rule {
 	for _, v := range nums {
 		id2 := fmt.Sprint(k, "_", v)
 		g.AddNewVarChange(k, id, id2)
-		ty := g.variables.lookupType(k, nil)
+		ty := g.variables.LookupType(k, nil)
 		if ty == "Bool" {
 			r := &rules.Infix{
 				X:  &rules.Wrap{Value: id},
@@ -332,9 +332,9 @@ func (g *Generator) capCond(b string, phis map[string]int16) ([]rules.Rule, map[
 		// when we produce the phi value for the first time
 		var id string
 		if phi, ok := phis[k]; !ok {
-			id = g.variables.advanceSSA(k)
-			g.declareVar(id, g.variables.lookupType(k, nil))
-			_, i := g.variables.getVarBase(id)
+			id = g.variables.AdvanceSSA(k)
+			g.declareVar(id, g.variables.LookupType(k, nil))
+			_, i := g.variables.GetVarBase(id)
 			g.addVarToRound(k, i)
 			phis[k] = int16(i)
 		} else {
@@ -359,14 +359,14 @@ func (g *Generator) capCondSyncRules(branches []string) map[string][]rules.Rule
 		fork := g.getCurrentFork()
 		for k, c := range fork {
 			if len(c) == 1 && c[0].Branch == b {
-				start := g.variables.getStartState(k)
-				id := g.variables.getSSA(k)
+				start := g.variables.GetStartState(k)
+				id := g.variables.GetSSA(k)
 				e = append(e, g.capRule(k, []int16{start}, id)...)
-				n := g.variables.ssa[k]
+				n := g.variables.SSA[k]
 				if g.inPhiState.Level() == 1 {
-					g.variables.newPhi(k, n)
+					g.variables.NewPhi(k, n)
 				} else {
-					g.variables.storeLastState(k, n)
+					g.variables.StoreLastState(k, n)
 				}
 			}
 		}