Commit 59e699fa authored by Hugo Moreau's avatar Hugo Moreau
Browse files

Boilerplate: Handling config.json file

It is now possible to load a config file in order to do two things :
 - Display all saved formulae.
 - Pick a formula using the index (/!\ Be careful, the `-ltl` flag will
   be overwriten, a warning is displayed for the user.)

 * boilerplate/config/config.go : New file.
   boilerplate/main.go,
   main.go : Modified.
parent 134e7fc9
package config
import (
"bufio"
"encoding/json"
"fmt"
"os"
"strings"
)
// Custom config
type Config struct {
Formulae []string `json:"formulae"`
}
// Jsonify fromats a file into a single string.
func Jsonify(filename string) string {
input, err := os.Open(filename)
if err != nil {
fmt.Println(os.Stderr, err)
os.Exit(2)
}
res := ""
scanner := bufio.NewScanner(input)
for scanner.Scan() {
res += scanner.Text()
}
return res
}
// LoadConfig load a config file based on json encoding.
func LoadConfig(filename string) Config {
var res Config
configJson := Jsonify(filename)
if err := json.Unmarshal([]byte(configJson), &res); err != nil {
panic(err)
}
return res
}
// DisplayFormulae diaplays all formulae contained in Config struct.
func (c *Config) DisplayFormulae() {
if len(c.Formulae) == 0 {
fmt.Println("No formula have been saved")
return
}
fmt.Printf("There are currently %d formula saved :\n", len(c.Formulae))
for key, formula := range c.Formulae {
fmt.Printf("\t %d - %s\n", key, formula)
}
}
var reachKeyWords []string = []string{"EMPTY", "NOTEMPTY"}
func find(array []string, x string) bool {
for _, val := range array {
if val == x {
return true
}
}
return false
}
// PickFormula selects the requested formula.
// PickFormula triggers an error whenever the index is incorrect.
// If the formula is from a Reach Problem, it will ignore the first word.
func (c *Config) PickFormula(index int) string {
if index < 0 || index >= len(c.Formulae) {
fmt.Printf("Given index %d is incorrect, please pick a formula from this list :\n", index)
c.DisplayFormulae()
os.Exit(2)
}
res := c.Formulae[index]
resArray := strings.Fields(res)
if find(reachKeyWords, resArray[0]) {
res = strings.Join(resArray[1:], " ")
}
fmt.Printf("Formula selected :\n %s\n", res)
return res
}
......@@ -26,11 +26,13 @@ package {{.PackageName}}
import "C"
import (
"{{.Output}}/structs"
"{{.Output}}/config"
"flag"
"fmt"
"log"
"os"
"os/exec"
path_ "path"
"path/filepath"
"regexp"
"strconv"
......@@ -357,6 +359,8 @@ var (
help = flag.Bool("help", false, "Show usages.")
backend = flag.String("backend", "spot", "[spot|ltsmin] The model-checking backend to use")
display = flag.Bool("display", false, "Display the state-space in DOT (only spot backend)")
formula = flag.Int("formula", -1, "Pick up the desired formula from config.json")
formulae = flag.Bool("formulae", false, "Display the saved formulae in config.json")
kripke_ss = flag.Bool("kripke-size", false, "The size of the state space (only spot backend)")
list_var = flag.Bool("list-variables", false, "Display the list of variable names.")
ltl = flag.String("ltl", "", "The LTL formulae to check")
......@@ -423,6 +427,19 @@ func main() {
path = filepath.Dir(path)
maindve2C := path + "/main.dve2C"
if *formulae {
config := config.LoadConfig(path_.Join(path,"config.json"))
config.DisplayFormulae()
}
if *formula != -1 {
if *ltl != "" {
fmt.Println("Rewriting given LTL formula")
}
config := config.LoadConfig(path_.Join(path,"config.json"))
*ltl = config.PickFormula(*formula)
}
if *list_var {
fmt.Println("State size:", structs.G2PStateSize)
......
......@@ -612,6 +612,11 @@ func main() {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
// Create the config package
if err := os.MkdirAll(path.Join(*output, "config"), 0777); err != nil {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
// Get project root directory to locate boilerplate/ dir
_, currentPath, _, ok := runtime.Caller(0)
if !ok {
......@@ -719,6 +724,7 @@ func main() {
"Makefile",
"go2pins.c",
"go2pins.h",
"config/config.go",
"main.go",
}
data := packageTemplate{basePackagePath, packageName, *output}
......
Supports Markdown
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