Commit e29fbbd2 authored by Antoine Martin's avatar Antoine Martin Committed by Etienne Renault

ltl: implement basic desugar

parent d9c83053
package main
import (
"fmt"
"strings"
)
func Desugar(formula string, aliases map[string][]string) (string, error) {
if !strings.Contains(formula, "any") && !strings.Contains(formula, "all") {
return formula, nil
}
var b strings.Builder
for len(formula) > 0 {
op := ""
if strings.HasPrefix(formula, "any(") {
op = "||"
} else if strings.HasPrefix(formula, "all(") {
op = "&&"
}
// no keyword found, keep going
if op == "" {
b.WriteByte(formula[0])
formula = formula[1:]
continue
}
formula = formula[len("xxx("):]
xp, xpLen, err := findExpr(formula)
if err != nil {
return "", fmt.Errorf("couldn't expand expression: %v", err)
}
x, err := parseExpr(xp)
if err != nil {
return "", fmt.Errorf("couldn't parse expression '%s': %v", xp, err)
}
expanded, err := x.Expand(aliases, op)
if err != nil {
return "", fmt.Errorf("couldn't expand expression '%s': %v", xp, err)
}
b.WriteString(expanded)
// skip expression + closing parenthesis
formula = formula[xpLen+1:]
}
return b.String(), nil
}
func findExpr(formula string) (string, int, error) {
idx := strings.Index(formula, ")")
if idx == -1 {
return "", 0, fmt.Errorf("couldn't find closing parenthesis: %s", formula)
}
return formula[:idx], idx, nil
}
func parseExpr(expr string) (Expression, error) {
return &SimpleVar{
name: expr[1 : len(expr)-1],
}, nil
}
// SimpleVar represents a single variable expression
type SimpleVar struct {
name string
}
// BoolExpression represents a boolean expression, such as 'a == 2'
type BoolExpression struct {
lhs string
operator string
rhs string
}
type Expression interface {
Expand(aliases map[string][]string, op string) (string, error)
}
func (sv *SimpleVar) Expand(aliases map[string][]string, op string) (string, error) {
al, ok := aliases[sv.name]
if !ok {
return "", fmt.Errorf("couldn't find aliases for %s", sv.name)
}
if len(al) == 0 {
return "", fmt.Errorf("aliases list for %s is empty", sv.name)
}
var b strings.Builder
b.WriteString("(")
for i, alias := range al {
if i != 0 {
fmt.Fprintf(&b, " %s ", op)
}
fmt.Fprintf(&b, "\"%s\"", alias)
}
b.WriteString(")")
return b.String(), nil
}
func (bx *BoolExpression) Expand(aliases map[string][]string, op string) (string, error) {
al, ok := aliases[bx.lhs]
if !ok {
return "", fmt.Errorf("couldn't find aliases for %s", bx.lhs)
}
if len(al) == 0 {
return "", fmt.Errorf("aliases list for %s is empty", bx.lhs)
}
var b strings.Builder
b.WriteString("(")
for i, alias := range al {
if i != 0 {
fmt.Fprintf(&b, " %s ", op)
}
fmt.Fprintf(&b, "(\"%s %s %s\")", alias, bx.operator, bx.rhs)
}
b.WriteString(")")
return b.String(), nil
}
package main
import "testing"
func TestUnchanged(t *testing.T) {
tests := []string{
"",
"F a",
"G \"any\"",
"F \"all\"",
}
for _, expected := range tests {
got, err := Desugar(expected, nil)
if err != nil {
t.Errorf("got error while desugaring '%s'", expected)
}
if expected != got {
t.Errorf("expected '%s', got '%s'", expected, got)
}
}
}
func TestSimpleVarExpand(t *testing.T) {
tests := []struct {
variable SimpleVar
aliases map[string][]string
expected string
shouldFail bool
}{
// 0
{
variable: SimpleVar{
name: "a",
},
aliases: map[string][]string{
"a": []string{
"a1",
"a2",
"a3",
"a4",
},
},
expected: `("a1" || "a2" || "a3" || "a4")`,
shouldFail: false,
},
}
for i, test := range tests {
got, err := test.variable.Expand(test.aliases, "||")
if err != nil && !test.shouldFail {
t.Errorf("test %d returned an error: %v", i, err)
}
if err == nil && test.shouldFail {
t.Errorf("test %d didn't return an error: %v", i, err)
}
if got != test.expected {
t.Errorf("test %d: expected '%s', got '%s'", i, test.expected, got)
}
}
}
func TestBoolExpressionExpand(t *testing.T) {
tests := []struct {
expr BoolExpression
aliases map[string][]string
expected string
shouldFail bool
}{
// 0
{
expr: BoolExpression{
lhs: "a",
operator: "==",
rhs: "2",
},
aliases: map[string][]string{
"a": []string{
"a1",
"a2",
},
},
expected: `(("a1 == 2") || ("a2 == 2"))`,
shouldFail: false,
},
}
for i, test := range tests {
got, err := test.expr.Expand(test.aliases, "||")
if err != nil && !test.shouldFail {
t.Errorf("test %d returned an error: %v", i, err)
}
if err == nil && test.shouldFail {
t.Errorf("test %d didn't return an error: %v", i, err)
}
if got != test.expected {
t.Errorf("test %d: expected '%s', got '%s'", i, test.expected, got)
}
}
}
func TestDesugar(t *testing.T) {
tests := []struct {
formula string
aliases map[string][]string
expected string
shouldFail bool
}{
// 0
{
formula: `F any("a")`,
aliases: map[string][]string{
"a": []string{"a1", "a2"},
},
expected: `F ("a1" || "a2")`,
shouldFail: false,
},
}
for i, test := range tests {
got, err := Desugar(test.formula, test.aliases)
if err != nil && !test.shouldFail {
t.Errorf("test %d returned an error: %v", i, err)
}
if err == nil && test.shouldFail {
t.Errorf("test %d didn't return an error: %v", i, err)
}
if got != test.expected {
t.Errorf("test %d: expected '%s', got '%s'", i, test.expected, got)
}
}
}
package main
import "os"
import "fmt"
import "encoding/json"
func main() {
m := make(map[string][]string)
err := json.Unmarshal([]byte(os.Args[2]), &m)
if err != nil {
fmt.Fprintf(os.Stderr, "couldn't parse state map: %v\n", err)
os.Exit(1)
}
res, err := Desugar(os.Args[1], m)
if err != nil {
fmt.Fprintf(os.Stderr, "%v\n", err)
os.Exit(1)
}
fmt.Println("res: " + res)
}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment