Interface attempt 2 (#18)

* adding mermaid support

* moving visualizations to its own module

* adding tests

* giving up on mutation testing for now :( :( :(

* updating README

* Updated config.yml

* Updated config.yml

.circleci/config.yml

@@ -39,45 +39,45 @@ jobs:
       - store_test_results:
           path: /tmp/test-reports
 
-  mutate:
-    working_directory: ~/Fault
-    docker:
-      - image: cimg/go:1.17.5
-    parallelism: 4
-    steps:
-      - run:
-          name: Install LLVM
-          command: |
-            sudo apt-get update
-            sudo apt-get install llvm
-            sudo apt-get install git
-      - checkout
-      - restore_cache:
-          keys:
-            - go-mod-v5-{{ checksum "go.sum" }}
-      - run:
-          name: Install Dependencies
-          command: 
-            go mod download
-      - save_cache:
-          key: go-mod-v5-{{ checksum "go.sum" }}
-          paths:
-            - "/go/pkg/mod"
-      - run:
-          name: Install go-mutesting
-          command: |
-            git clone https://github.com/mbellotti/go-mutesting.git
-            cd go-mutesting
-            go build cmd/go-mutesting/main.go
-            chmod +x main
-            sudo mv main /usr/local/bin/go-mutesting
-      - run:
-          name: Mutate and take over the world
-          command: | # Don't test the fuzzer or main.go, for the time being skip execute because it needs to be rewritten
-            mkdir -p /tmp/test-mutate-reports
-            go-mutesting $(go list ./... | grep -v fault/execute | grep -v fault/parser | grep -v "^fault$" | circleci tests split) --fail-only --score=.52
-      - store_test_results:
-          path: /tmp/test-mutate-reports
+  # mutate:
+  #   working_directory: ~/Fault
+  #   docker:
+  #     - image: cimg/go:1.17.5
+  #   parallelism: 4
+  #   steps:
+  #     - run:
+  #         name: Install LLVM
+  #         command: |
+  #           sudo apt-get update
+  #           sudo apt-get install llvm
+  #           sudo apt-get install git
+  #     - checkout
+  #     - restore_cache:
+  #         keys:
+  #           - go-mod-v5-{{ checksum "go.sum" }}
+  #     - run:
+  #         name: Install Dependencies
+  #         command: 
+  #           go mod download
+  #     - save_cache:
+  #         key: go-mod-v5-{{ checksum "go.sum" }}
+  #         paths:
+  #           - "/go/pkg/mod"
+  #     - run:
+  #         name: Install go-mutesting
+  #         command: |
+  #           git clone https://github.com/mbellotti/go-mutesting.git
+  #           cd go-mutesting
+  #           go build cmd/go-mutesting/main.go
+  #           chmod +x main
+  #           sudo mv main /usr/local/bin/go-mutesting
+  #     - run:
+  #         name: Mutate and take over the world
+  #         command: | # Don't test the fuzzer or main.go, for the time being skip execute because it needs to be rewritten
+  #           mkdir -p /tmp/test-mutate-reports
+  #           go-mutesting $(go list ./... | grep -v fault/execute | grep -v fault/parser | grep -v "^fault$" | circleci tests split) --fail-only --score=.52
+  #     - store_test_results:
+  #         path: /tmp/test-mutate-reports
 
 
 # Invoke jobs via workflows
@@ -87,7 +87,7 @@ workflows:
     jobs:
       - test
 
-  mutations: # Scheduled pipeline, will run mutation tests once a week
-    unless: << pipeline.parameters.github >> 
-    jobs:
-      - mutate
+  # mutations: # Scheduled pipeline, will run mutation tests once a week
+  #   unless: << pipeline.parameters.github >> 
+  #   jobs:
+  #     - mutate

README.md

@@ -56,7 +56,10 @@ There are A LOT of assumptions there, so the pre-alpha development of Fault prio
 
 But then that's part of the fun too. Developing Fault is an opportunity to learn more about how SMT solvers (specifically Z3) work.
 
-### Current Status (11/30/2022)
+### Current Status (12/30/2022)
+Taking another stab at the interface question and display of results. Settled on using mermaid to visualize the solutions received from the solver which is much more useful than what I was trying otherwise. This reintroduces the dotviz generation from way back with the prototype so I've also included generated mermaid viz for the state machine and the active stock-flow subsystems.
+
+#### (11/30/2022)
 Trying to finish up state charts exposed some problems with conditionals that needed to be addressed, plus some bugs and funny edge cases. But state charts are now done, including a reachability analysis verifying that the system is appropriately specified that I think will be opt-in for now.
 
 #### (11/2/2022)

execute/execute.go

@@ -25,18 +25,21 @@ type Solver struct {
 }
 
 type ModelChecker struct {
-	SMT        string
-	Uncertains map[string][]float64
-	Unknowns   []string
-	solver     map[string]*Solver
-	forks      map[string][]*Branch
+	SMT          string
+	Uncertains   map[string][]float64
+	Unknowns     []string
+	Results      map[string][]*smt.VarChange
+	ResultValues map[string]string
+	solver       map[string]*Solver
+	forks        map[string][]*Branch
 }
 
 func NewModelChecker() *ModelChecker {
 
 	mc := &ModelChecker{
-		solver: GenerateSolver(),
-		forks:  make(map[string][]*Branch),
+		solver:       GenerateSolver(),
+		forks:        make(map[string][]*Branch),
+		ResultValues: make(map[string]string),
 	}
 	return mc
 }
@@ -62,10 +65,11 @@ func GenerateSolver() map[string]*Solver {
 	return s
 }
 
-func (mc *ModelChecker) LoadModel(smt string, uncertains map[string][]float64, unknowns []string) {
+func (mc *ModelChecker) LoadModel(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) {
 	mc.SMT = smt
 	mc.Uncertains = uncertains
 	mc.Unknowns = unknowns
+	mc.Results = results
 }
 
 func (mc *ModelChecker) LoadMeta(forks []smt.Fork) {
@@ -140,6 +144,8 @@ func (mc *ModelChecker) Solve() (map[string]Scenario, error) {
 	l := NewSMTListener()
 	antlr.ParseTreeWalkerDefault.Walk(l, p.Start())
 
+	mc.ResultValues = l.Values
+
 	return l.Results, err
 }
 

execute/execute_test.go

@@ -1,6 +1,9 @@
 package execute
 
-import "testing"
+import (
+	"fault/smt"
+	"testing"
+)
 
 func TestSMTOk(t *testing.T) {
 	test := `(declare-fun imports_fl3_vault_value_0 () Real)
@@ -9,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{})
+	model := prepTest(test, make(map[string][]float64), []string{}, map[string][]*smt.VarChange{})
 
 	response, err := model.Check()
 
@@ -48,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{})
+	model := prepTest(test, uncertains, []string{}, map[string][]*smt.VarChange{})
 
 	model.Check()
 	solution, _ := model.Solve()
@@ -61,8 +64,8 @@ func TestProbability(t *testing.T) {
 
 }
 
-func prepTest(smt string, uncertains map[string][]float64, unknowns []string) *ModelChecker {
+func prepTest(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) *ModelChecker {
 	ex := NewModelChecker()
-	ex.LoadModel(smt, uncertains, unknowns)
+	ex.LoadModel(smt, uncertains, unknowns, results)
 	return ex
 }

execute/format.go

@@ -2,6 +2,7 @@ package execute
 
 import (
 	"bytes"
+	"fault/smt"
 	"fmt"
 	"strings"
 )
@@ -11,6 +12,39 @@ import (
  checker in user friendly ways
 */
 
+func (mc *ModelChecker) Mermaid() {
+	var out bytes.Buffer
+	out.WriteString("flowchart LR\n")
+	for k, l := range mc.Results {
+		out.WriteString(mc.writeObjects(k, l))
+		out.WriteString("\n")
+	}
+	fmt.Println(out.String())
+}
+
+func (mc *ModelChecker) writeObjects(k string, objects []*smt.VarChange) string {
+	var objs []string
+	for _, o := range objects {
+		if o.Parent != "" {
+			objs = append(objs, mc.writeObject(o))
+		}
+	}
+	last := objects[len(objects)-1]
+	value := mc.ResultValues[last.Id]
+	cap := fmt.Sprintf("\t% s--> %s(%s)", last.Id, k, value)
+	objs = append(objs, cap)
+	return strings.Join(objs, "\n")
+}
+
+func (mc *ModelChecker) writeObject(o *smt.VarChange) string {
+	value, ok := mc.ResultValues[o.Parent]
+	if ok {
+		return fmt.Sprintf("\t% s--> |%s| %s", o.Parent, value, o.Id)
+	} else {
+		return fmt.Sprintf("\t%s --> %s", o.Parent, o.Id)
+	}
+}
+
 func (mc *ModelChecker) Format(results map[string]Scenario) {
 	var out bytes.Buffer
 	//results = definePath(results, mc.forks)

execute/responses.go

@@ -11,11 +11,13 @@ type SMTListener struct {
 	*parser.BaseSMTLIBv2Listener
 	stack   []interface{}
 	Results map[string]Scenario
+	Values  map[string]string
 }
 
 func NewSMTListener() *SMTListener {
 	return &SMTListener{
 		Results: make(map[string]Scenario),
+		Values:  make(map[string]string),
 	}
 }
 
@@ -45,7 +47,14 @@ func (l *SMTListener) ExitFunction_def(c *parser.Function_defContext) {
 	sort := l.pop()
 	sym := l.pop()
 
-	value := convertTerm(sort.(string), term.(string))
+	t := term.(string)
+	if string(t[0]) == "(" { // Happens in negative values
+		t = t[1 : len(t)-2]
+	}
+
+	l.Values[sym.(string)] = t
+
+	value := convertTerm(sort.(string), t)
 	key, id := splitIdent(sym.(string))
 	i, err := strconv.ParseInt(key, 10, 16)
 	k := int16(i)
@@ -98,10 +107,6 @@ func convertTerm(sort string, term string) interface{} {
 	var value interface{}
 	var err error
 
-	if string(term[0]) == "(" {
-		term = term[1 : len(term)-2]
-	}
-
 	switch sort {
 	case "Real":
 		value, err = strconv.ParseFloat(term, 64)

main.go

@@ -11,6 +11,7 @@ import (
 	"fault/smt"
 	"fault/types"
 	"fault/util"
+	"fault/visualize"
 	"flag"
 	"fmt"
 	"log"
@@ -22,7 +23,7 @@ import (
 	_ "github.com/olekukonko/tablewriter"
 )
 
-func parse(data string, path string, file string, filetype string, reach bool) (*listener.FaultListener, *types.Checker) {
+func parse(data string, path string, file string, filetype string, reach bool, visu bool) (*listener.FaultListener, *types.Checker, string) {
 	// Setup the input
 	is := antlr.NewInputStream(data)
 
@@ -57,11 +58,18 @@ func parse(data string, path string, file string, filetype string, reach bool) (
 		log.Fatal(err)
 	}
 
+	var visual string
+	if visu {
+		vis := visualize.NewVisual(tree)
+		vis.Build()
+		visual = vis.Render()
+	}
+
 	if reach {
 		r := reachability.NewTracer()
 		r.Scan(tree)
 	}
-	return lstnr, ty
+	return lstnr, ty, visual
 }
 
 func ll(lstnr *listener.FaultListener, ty *types.Checker) *llvm.Compiler {
@@ -81,9 +89,9 @@ func smt2(ir string, uncertains map[string][]float64, unknowns []string, asserts
 	return generator
 }
 
-func probability(smt string, uncertains map[string][]float64, unknowns []string) (*execute.ModelChecker, map[string]execute.Scenario) {
+func probability(smt string, uncertains map[string][]float64, unknowns []string, results map[string][]*smt.VarChange) (*execute.ModelChecker, map[string]execute.Scenario) {
 	ex := execute.NewModelChecker()
-	ex.LoadModel(smt, uncertains, unknowns)
+	ex.LoadModel(smt, uncertains, unknowns, results)
 	ok, err := ex.Check()
 	if err != nil {
 		log.Fatal(err)
@@ -119,7 +127,7 @@ func run(filepath string, mode string, input string, reach bool) {
 
 	switch input {
 	case "fspec":
-		lstnr, ty := parse(d, path, filepath, filetype, reach)
+		lstnr, ty, visual := parse(d, path, filepath, filetype, reach, mode == "visualize")
 		if lstnr == nil {
 			log.Fatal("Fault parser returned nil")
 		}
@@ -144,7 +152,13 @@ func run(filepath string, mode string, input string, reach bool) {
 			return
 		}
 
-		mc, data := probability(generator.SMT(), uncertains, unknowns)
+		mc, data := probability(generator.SMT(), uncertains, unknowns, generator.Results)
+		if mode == "visualize" {
+			fmt.Println(visual)
+			fmt.Printf("\n\n")
+			mc.Mermaid()
+			return
+		}
 		mc.LoadMeta(generator.GetForks())
 		fmt.Println("~~~~~~~~~~\n  Fault found the following scenario\n~~~~~~~~~~")
 		mc.Format(data)
@@ -155,13 +169,21 @@ func run(filepath string, mode string, input string, reach bool) {
 			return
 		}
 
-		mc, data := probability(generator.SMT(), uncertains, unknowns)
+		mc, data := probability(generator.SMT(), uncertains, unknowns, generator.Results)
+		if mode == "visualize" {
+			mc.Mermaid()
+			return
+		}
 		mc.LoadMeta(generator.GetForks())
 		fmt.Println("~~~~~~~~~~\n  Fault found the following scenario\n~~~~~~~~~~")
 		mc.Format(data)
 	case "smt2":
-		mc, data := probability(d, uncertains, unknowns)
+		mc, data := probability(d, uncertains, unknowns, make(map[string][]*smt.VarChange))
 
+		if mode == "visualize" {
+			mc.Mermaid()
+			return
+		}
 		fmt.Println("~~~~~~~~~~\n  Fault found the following scenario\n~~~~~~~~~~")
 		mc.Format(data)
 	}
@@ -195,6 +217,7 @@ func main() {
 		case "ir":
 		case "smt":
 		case "check":
+		case "visualize":
 		default:
 			fmt.Printf("%s is not a valid mode\n", mode)
 			os.Exit(1)