Commit 78f827c6 authored by Etienne Renault's avatar Etienne Renault
Browse files

More options for go2pins-mc

* README.md, benchs/run-benchmark.sh,
boilerplate/main.go: Here.
parent 042c20c5
......@@ -25,9 +25,17 @@ go build
cd output
make
# Then, to generate the state tree of your program, you can use Spot's
# modelcheck utility (in tests/ltsmin/modelcheck)
modelcheck -gm main.dve2C "G(true)" | tail -n +2 > my_program.dot
# Then, to generate the state tree of your program and if you have
# use Spot's modelcheck utility in your PATH (in tests/ltsmin/modelcheck)
./go2pins-mc -display
# You can also perform LTL model checking by running either
./go2pins-mc '<some_ltl_formula>' --backend spot
# or if you have LTSmin backend installed
./go2pins-mc '<some_ltl_formula>' --backend ltsmin
# Note that the LTL syntax may differ according to the various backend.
```
## Limitations
......
......@@ -54,7 +54,7 @@ for model in $FILES; do
echo " - Total Time:\t\t\t$total_time seconds"
final_num_var=$($filename/main --list-variables | grep '\-' | wc -l)
final_num_var=$($filename/go2pins-mc --list-variables | grep '\-' | wc -l)
echo " - Number of variables:\t\t$final_num_var"
loc2=$(wc -l $filename/$filename.go| tail -n1|awk '{print $1}')
......
......@@ -9,7 +9,9 @@ import "C"
import (
"flag"
"fmt"
"log"
"os"
"os/exec"
"unsafe"
)
......@@ -325,8 +327,11 @@ func get_guard_nds_matrix(g C.int) *C.int {
// ------------------------------------------------------------
var (
list_var = flag.Bool("list-variables", false, "Display the list of variable names.")
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)")
list_var = flag.Bool("list-variables", false, "Display the list of variable names.")
ltl = flag.String("ltl", "", "The LTL formulae to check")
)
func init() {
......@@ -336,12 +341,33 @@ func init() {
}
}
func spot_path() string {
path, err := exec.LookPath("modelcheck")
if err != nil {
panic("\n\tSpot backend not aivalable! Update your PATH to have modelcheck in it.\n\texport PATH=<path_to_spot>/tests/ltsmin/:$PATH")
}
fmt.Println("Using : ", path)
return path
}
func ltsmin_path() string {
path, err := exec.LookPath("dve2lts-mc")
if err != nil {
panic("\n\tLTSmin backend not aivalable! Update your PATH to have dve2lts-mc in it.\n\texport PATH=<path_to_ltsmin>/bin/:$PATH")
}
fmt.Println("Using : ", path)
return path
}
func main() {
flag.Parse()
if len(os.Args) == 1 || *help {
flag.Usage()
os.Exit(1)
}
if *list_var {
fmt.Println("State size:", G2PStateSize)
fmt.Println("List of variable names:")
......@@ -349,4 +375,37 @@ func main() {
fmt.Println(" - " + C.GoString(G2PVariableNames[i]))
}
}
if *ltl != "" {
var mcCmd *exec.Cmd
if *backend == "ltsmin" {
mcCmd = exec.Command(ltsmin_path(), "--threads", "1",
"--ltl", *ltl, "main.dve2C")
} else if *backend == "spot" || *backend == "" {
mcCmd = exec.Command(spot_path(), "main.dve2C", *ltl)
} else {
panic("backend '" + *backend + "' unknown!")
}
mcCmd.Stdout = os.Stdout
mcCmd.Stderr = os.Stderr
err := mcCmd.Run()
if err != nil {
log.Fatalf("command failed with %s\n", err)
}
mcOut, err := mcCmd.Output()
fmt.Println(string(mcOut))
}
if *display {
mcCmd := exec.Command(spot_path(), "-gm", "main.dve2C", "true")
mcCmd.Stdout = os.Stdout
mcCmd.Stderr = os.Stderr
err := mcCmd.Run()
if err != nil {
log.Fatalf("command failed with %s\n", err)
}
mcOut, err := mcCmd.Output()
fmt.Println(string(mcOut))
}
}
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