Automatize RERS inputs

Until now, user had to enter the correct RERS inputs in order to use it, it was so boring:

go2pins -rers "4;2;3;1;5" ProblemXX-XXX.go

For a better experience, RERS input are automatically detected in RERS file, just invoke Go2Pins with the -rers flag.

go2pins -rers ProblemXX-XXX.go

This enhancement comes with the goal to make Go2Pins an user-friendly tool.

Automatizing Blackbox transformation via LTL formulae

As we saw last week, we can generate a fully blackboxed file based on a given LTL formulae file.
First of all there was a little thing we needed to correct, with the formulae process, the main function could be ignored. Since without any functions, our program won’t work, it is now corrected. We can start the real things.

Automatizing ? Yes but not everything

By giving a LTL formulae file to Go2Pins this way:

go2pins -ltl formulae.txt program.go

- “All non essentials function will be blackboxed, great !”
- “Really ?”
- “Yes, really, don’t doubt about it !”
- “But if we want to analyse one formula ?”
- “Yeah… I guess…”
- “And if we don’t want to blackbox our function everytime ?”
- “Okay, I got it…”
We need to manipulate one formula and not every formulae, and automatic blackbox should be automatic only if we ask for it.
Since more than one formula is already too many to decide if we want blackbox or not, calling Go2pins with the formulae flag will automatically trigger the blackbox automatization, if the user want to decide himself, I guess he will just call with blackbox-fn flag and not the formulae one.

One formula and no more

If you read my blog from the beggining, you are already familiar with Go2Pins and its using, but because there may be some new one, let’s show them what it looks like to use it.

go2pins [options] <file>

It seems a little bit easy like that, but there are many options, right now, we don’t care about it, or maybe just one we already created, the formulae one. It takes a formulae file and will establish in the call graph which function, we will use that again but instead of having a list of formulae, we will just have one. Nothing complicated. So ? A new flag ? No, let’s say it is now an optional argument.

go2pins [options] <file> [formula]

Good, we know where is stored our formula, by giving a formula, we will call a model checking tool (let’s say (Spot)[https://spot.lrde.epita.fr/]) in order to analyse it.

❯ go2pins -f benchs/RERS/2016-Problem1-ltl.go "(! \"main_final_output == 22\" W \"main_main___RERS__ == 2\")"
Using :  /home/ryuki/Downloads/spot-2.8.5/tests/ltsmin/modelcheck
[Go2Pins] have_property: unimplemented ... SKIP
75 unique states visited
0 strongly connected components in search stack
75 transitions explored
75 items max in DFS search stack
993 pages allocated for emptiness check
no accepting run found

Before all of that, user needed to go in the output directory and call go2pins-mc in order to have the same result, it was fastidious, so it is now changed.\ No more for now.

Automatizing Blackbox based on a formula

No more for now, I said ? Not really, now we have that, don’t forget our Blackbox, how to automatize it ? Sinmply by reusing our formulae function we created and let’s add something that triggers it, the keyword auto passed to blackbox-fn flag seems a good idea. Okay, let’s see what it gives with the same example:

❯ go2pins -f -blackbox-fn="auto" benchs/RERS/2016-Problem1-ltl.go "(! \"main_final_output == 22\" W \"main_main___RERS__ == 2\")"
Using :  /home/ryuki/Downloads/spot-2.8.5/tests/ltsmin/modelcheck
[Go2Pins] have_property: unimplemented ... SKIP
32 unique states visited
0 strongly connected components in search stack
32 transitions explored
32 items max in DFS search stack
576 pages allocated for emptiness check
no accepting run found

Recap

  • Go2pins now takes an optional argument that is a formula.
  • The auto keyword used in blackbox-fn flag now triggers the automatization process for Blackbox if a formula is given.
  • RERS inputs no longer need to be given, Go2Pins will find it automatically.
  • And all this contributes to make Go2Pins more user friendly.

Links and more

SHA1 of the week

References