Global array variables in Blackbox functions

Global array are not treated yet in the Blackbox package, since we need to add more transform to the process. Good thing for us we already have a transform that does the job, DoubleBrackets. So here we go, let’s use it, let’s suppose we have a global variable that is an array:

my_array[2] = 0

Before our transform, we did locate my_array as a variable, but we didn’t know it was an array, resulting to something like this:

G2PState[4][2] = 0

So the trick is to detect when there is an IndexExpr nested in another and we can easily obtain this:

G2PState[4 + 2] = 0

So global arrays are now handled in our Blackbox.

Nested Index Expression ? Multidimensional array ?

Good, we can use global array, and none global as well, but (there is always a “but” if you didn’t realize) what if we have this:

my_array[your_array[1]]

or this:

our_array[2][3]

Funny to guess, it is not yet handled, so here we go.

Nested Index Expression

Let’s take again our example:

my_array[your_array[1]]

Go2Pins will transform this as:

G2PState[4][G2PState[10][1]]

So you can see, it’s a just a recursion story, we need to travel our Abstract Syntax Tree, and whenever we encounter an IndexExpr, we just have to check its children and if it’s once again an IndexExpr, we continue until there is no more, in our case a Ident(https://golang.org/pkg/go/ast/#Ident). Let’s take a look on this new change, and what it looks like now:

G2PState[4 + G2PState[10 + 1]]

Want to have a look on this ? Here it is:

Mutltidimensional array

Okay, multidimensional array, what if we do this another day ? Why ? May I explain you how the current arrays are transformed.
Let’s say we have an array with 5 elements:

var a int[] = []int{0, 1, 2, 3, 4}

Nothing complicated, the way Go2Pins handle it is creating one variable for each position in our array, in our case, 5 variables:

a := 0
a_1 := 1
a_2 := 2
a_3 := 3
a_4 := 4

Note that the first variable is not indexed as the other.
So with this technique, we can easily transform a multidimensional array as a one-dimensional array and then apply our transform.

var arr [][]int = [][]int{{0, 1, 2}, {3, 4, 5}}

Let’s say we want to access to the second element of the second array in arr. We just use arr[1][1], but with a single-dimensionnal array, it would just be arr[1*len(arr[0])+1], so nothing complicated if we consider that we have fixed len in our array. Where it becomes more complicated is when we hold more than two dimensions:

var arr [][][]int = [][][]int{{{0, 1, 2}, {3, 4, 5}}, {{6, 7, 8}, {9, 10, 11}}}

We have an array of size 2 containing arrays of size 2 containing 3 elements, so 12 elements for a single-dimensional array, or a two-dimensionnal array of 2 arrays of 6 elements. Accessing to arr[1][0][1] is accessing at arr[1*6+0*3+1], it makes senses, but it requires a little work on it, since it would ask me to create a new transform and I don’t know how Go2Pins will work in the future, I will let this idea here and maybe pick it if needed.

So I decided to check if we had Multidimensionnal array and panic if encountered.

Benchmarking our Blackbox transitions

I worked for nearly two months to make blackbox transitions more viable, and we already saw some good results.
Let’s say now we want more, but benchmarking all of this will take a lot of time, we want some good methods to do it, so we decided to make a Makefile, because in the case our benchmark stops for a reason, we want to launch it again and not to have to rebuild all the benchmark.
The Makefile will build three csv files, one for the LTL problems, one for the Reachibility problems and one global regrouping the compile memory and time.
For the LTL and Reachibility problems, we will globally evalutate the appropriate formulae.
I won’t go in too much details here, because I want to always be clear on what I do.
You can find the Makefile here.

You already know everything about what we did, and if not, you can just read the previous articles.
We have two dozens of RERS Problems files we need to compute and compare results between Blackbox and no Blackbox involved in order to see the difference and declare if yes or no, our approach is a good one. So once we have it, I will be happy to share it with you.
Just to tease you a little you a little bit:

FileFormulaStatesTransitionsBlackbox StatesBlackbox Transitions
2016-Problem1-ltl.go(! "main_final_output == 22" W "main_main___RERS__ == 2")11711150985981228

Links and more

References