Commit b175b0a9 authored by Etienne Renault's avatar Etienne Renault

boilerplate: fix compability with Spot's dev version

* boilerplate/main.go: Here.
parent 0cad5bd5
Pipeline #20392 passed with stage
in 1 minute and 47 seconds
......@@ -394,6 +394,24 @@ func spot_path() string {
return path
}
type DevNull struct{}
func (DevNull) Write(p []byte) (int, error) {
return len(p), nil
}
func spot_dev_version() bool {
path, _ := exec.LookPath("modelcheck")
mcCmd := exec.Command(path, "--version")
mcCmd.Stdout = new(DevNull)
mcCmd.Stderr = new(DevNull)
err := mcCmd.Run()
if err != nil {
return false
}
return true
}
func ltsmin_path() string {
path, err := exec.LookPath("dve2lts-mc")
if err != nil {
......@@ -406,6 +424,7 @@ func ltsmin_path() string {
func main() {
flag.Parse()
if len(os.Args) == 1 || *help {
flag.Usage()
os.Exit(1)
......@@ -425,7 +444,13 @@ func main() {
mcCmd = exec.Command(ltsmin_path(), "--threads", "1",
"--ltl", *ltl, "main.dve2C")
} else if *backend == "spot" || *backend == "" {
mcCmd = exec.Command(spot_path(), "main.dve2C", "!"+*ltl)
if !spot_dev_version() {
mcCmd = exec.Command(spot_path(), "main.dve2C", "!"+*ltl)
} else {
mcCmd = exec.Command(spot_path(), "-e",
"--model", "main.dve2C",
"--formula", "!"+*ltl)
}
} else {
panic("backend '" + *backend + "' unknown!")
}
......@@ -441,7 +466,12 @@ func main() {
}
if *display {
mcCmd := exec.Command(spot_path(), "-gm", "main.dve2C", "true")
var mcCmd *exec.Cmd
if !spot_dev_version() {
mcCmd = exec.Command(spot_path(), "-gm", "main.dve2C", "true")
} else {
mcCmd = exec.Command(spot_path(), "--model", "main.dve2C", "--dot=model")
}
mcCmd.Stdout = os.Stdout
mcCmd.Stderr = os.Stderr
err := mcCmd.Run()
......@@ -453,7 +483,16 @@ func main() {
}
if *kripke_ss {
out, _ := exec.Command(spot_path(), "main.dve2C", "F \"LabelCounter==-1\"").Output()
var out []byte
if !spot_dev_version() {
out, _ = exec.Command(spot_path(), "main.dve2C", "F \"LabelCounter==-1\"").Output()
} else {
out, _ = exec.Command(spot_path(), "-e",
"--model", "main.dve2C",
"--formula", "F \"LabelCounter==-1\"").Output()
}
output := string(out[:])
r, _ := regexp.Compile(".*unique.*")
r1, _ := regexp.Compile(".*transitions.*")
......
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