Commit 4096a93e authored by Etienne Renault's avatar Etienne Renault

output: ease user's life

Typing "make -C output" is now obsolete

* boilerplate/main.go,
main.go: Here.
parent 2d5a8045
Pipeline #24012 passed with stage
in 1 minute and 51 seconds
......@@ -30,6 +30,7 @@ import (
"log"
"os"
"os/exec"
"path/filepath"
"regexp"
"strings"
"unsafe"
......@@ -430,6 +431,14 @@ func main() {
os.Exit(1)
}
path, err := os.Executable()
if err != nil {
log.Println(err)
}
path = filepath.Dir(path)
maindve2C := path + "/main.dve2C"
if *list_var {
fmt.Println("State size:", G2PStateSize)
fmt.Println("List of variable names:")
......@@ -442,13 +451,13 @@ func main() {
var mcCmd *exec.Cmd
if *backend == "ltsmin" {
mcCmd = exec.Command(ltsmin_path(), "--threads", "1",
"--ltl", *ltl, "main.dve2C")
"--ltl", *ltl, maindve2C)
} else if *backend == "spot" || *backend == "" {
if !spot_dev_version() {
mcCmd = exec.Command(spot_path(), "main.dve2C", "!"+*ltl)
mcCmd = exec.Command(spot_path(), maindve2C, "!"+*ltl)
} else {
mcCmd = exec.Command(spot_path(), "-e",
"--model", "main.dve2C",
"--model", maindve2C,
"--formula", "!"+*ltl)
}
} else {
......@@ -468,9 +477,9 @@ func main() {
if *display {
var mcCmd *exec.Cmd
if !spot_dev_version() {
mcCmd = exec.Command(spot_path(), "-gm", "main.dve2C", "true")
mcCmd = exec.Command(spot_path(), "-gm", maindve2C, "true")
} else {
mcCmd = exec.Command(spot_path(), "--model", "main.dve2C", "--dot=model")
mcCmd = exec.Command(spot_path(), "--model", maindve2C, "--dot=model")
}
mcCmd.Stdout = os.Stdout
mcCmd.Stderr = os.Stderr
......@@ -486,10 +495,10 @@ func main() {
var out []byte
if !spot_dev_version() {
out, _ = exec.Command(spot_path(), "main.dve2C", "F \"LabelCounter==-1\"").Output()
out, _ = exec.Command(spot_path(), maindve2C, "F \"LabelCounter==-1\"").Output()
} else {
out, _ = exec.Command(spot_path(), "-e",
"--model", "main.dve2C",
"--model", maindve2C,
"--formula", "F \"LabelCounter==-1\"").Output()
}
......
......@@ -30,6 +30,7 @@ import (
"io"
"io/ioutil"
"os"
"os/exec"
"path"
"regexp"
"runtime"
......@@ -577,11 +578,15 @@ func main() {
copyFile(from, to, data)
}
fmt.Println("Preprocessing done.\n\nTo display statistics about the state space of you program, follows the instructions below")
fmt.Println(" cd", *output)
fmt.Println(" make")
fmt.Println(" ./go2pins-mc -kripke-size")
fmt.Println("\nDisplay all available options (including LTL verification) with the following instruction:")
fmt.Println(" ./go2pins-mc -help")
// Ease users life, do not force them to make by themself
cmd := exec.Command("make", "-C", *output)
_, err = cmd.Output()
if err != nil {
fmt.Println(err.Error())
return
}
fmt.Println("Preprocessing done.\n")
fmt.Println("Display all available options (including LTL verification) by running:")
fmt.Println(" ./" + *output + "/go2pins-mc -help\n")
}
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