Refactoring smt (#23)

* tightening up the functions around VarRounds * breaking out assert/assume generation into smaller functions * renaming parse functions that don't involve parsing to create XXX rule functions * moving rules to their own subpackage * moving variable data over to own package and starting generator * moving fork logic to its own package * cleaning up and consolidating old test files * updating command line interface to be consistent across Docker and main.go
Fault-lang · Feb 23, 2023 · 2b993de · 2b993de
1 parent 0e1ef98
commit 2b993de
Show file tree

Hide file tree

Showing 25 changed files with 3,293 additions and 3,294 deletions.
diff --git a/execute/execute.go b/execute/execute.go
@@ -4,7 +4,8 @@ import (
 	"bytes"
 	"errors"
 	"fault/execute/parser"
-	"fault/smt"
+	"fault/smt/forks"
+	"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,19 +66,19 @@ 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
 	mc.Results = results
 }
 
-func (mc *ModelChecker) LoadMeta(forks []smt.Fork) {
+func (mc *ModelChecker) LoadMeta(frks []forks.Fork) {
 	// Load metadata that helps the results display nicely
 	tree := make(map[string][]*Branch)
-	for _, f := range forks {
+	for _, f := range frks {
 		for k, c := range f {
-			ends := smt.GetForkEndPoints(c)
+			ends := forks.GetForkEndPoints(c)
 			phi := util.MaxInt16(ends)
 			var branches []*Branch
 			for _, v := range c {

diff --git a/execute/execute_test.go b/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

diff --git a/execute/format.go b/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)

diff --git a/execute/format_test.go b/execute/format_test.go
@@ -1,7 +1,7 @@
 package execute
 
 import (
-	"fault/smt"
+	"fault/smt/forks"
 	"testing"
 )
 
@@ -16,8 +16,8 @@ func TestPhis(t *testing.T) {
 		weights: map[int16]float64{},
 	}
 
-	phis := []smt.Fork{{
-		"test_value": []*smt.Choice{
+	phis := []forks.Fork{{
+		"test_value": []*forks.Choice{
 			{
 				Base:   "test_value",
 				Values: []int16{1},
@@ -27,7 +27,7 @@ func TestPhis(t *testing.T) {
 				Values: []int16{3},
 			},
 		},
-		"test_value_foo": []*smt.Choice{
+		"test_value_foo": []*forks.Choice{
 			{
 				Base:   "test_value_foo",
 				Values: []int16{1, 3, 4},
@@ -72,8 +72,8 @@ func TestMultiPhis(t *testing.T) {
 		weights: map[int16]float64{},
 	}
 
-	phis := []smt.Fork{{
-		"test_value": []*smt.Choice{
+	phis := []forks.Fork{{
+		"test_value": []*forks.Choice{
 			{
 				Base:   "test_value",
 				Values: []int16{1, 2},
@@ -84,7 +84,7 @@ func TestMultiPhis(t *testing.T) {
 			},
 		}},
 		{
-			"test_value": []*smt.Choice{
+			"test_value": []*forks.Choice{
 				{
 					Base:   "test_value",
 					Values: []int16{5, 6},

diff --git a/main.go b/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()
@@ -201,10 +202,10 @@ func main() {
 	var input string
 	var filepath string
 	var reach bool
-	modeCommand := flag.String("mode", "check", "stop compiler at certain milestones: ast, ir, smt, or check")
-	inputCommand := flag.String("input", "fspec", "format of the input file (default: fspec)")
-	fpCommand := flag.String("filepath", "", "path to file to compile")
-	reachCommand := flag.String("complete", "false", "make sure the transitions to all defined states are specified in the model")
+	modeCommand := flag.String("m", "check", "stop compiler at certain milestones: ast, ir, smt, or check")
+	inputCommand := flag.String("i", "fspec", "format of the input file (default: fspec)")
+	fpCommand := flag.String("f", "", "path to file to compile")
+	reachCommand := flag.String("c", "false", "make sure the transitions to all defined states are specified in the model")
 
 	flag.Parse()