ProductDfa segfaults with >2 specification inputs

[florisdenhengst]

The shield synthesis tool seems to be unable to handle more than two dfa file inputs.

Consider the following three input specifications:

==> /tmp/1.dfa <==
dfa 2 0 1 1 1 3
1
2
1 1 -1
1 2 1
2 2
1 mistake_1

==> /tmp/2.dfa <==
dfa 2 0 1 1 1 3
1
2
1 1 -1
1 2 1
2 2
1 mistake_2

==> /tmp/3.dfa <==
dfa 2 0 1 1 1 3
1
2
1 1 -1
1 2 1
2 2
1 mistake_3

These specifications are very simple. They have no input and a single output each, which should never be activated. As long as it not activated, the dfa stays in the initial (safe) state. If the output is activated, the dfa transitions into a final (unsafe) state. The winning strategy is !mistake_1 && !mistake_2 && !mistake3 all the time, any other strategy loses.

The tool works fine running any two of these inputs yet running all of them together gives the following output:

$./shield_synthesizer 1 toy-old /tmp/*.dfa
OUT: mistake_1
OUT: mistake_2
OUT: mistake_3
mistake_1has index 1
Adding shift index for var mistake_1: 0
mistake_2has index 2
Adding shift index for var mistake_2: 1
mistake_3has index 3
Adding shift index for var mistake_3: 2
Intial node: <1> or <[<1>,]>
Intial node: <3> or <[<1>,<1>,]>
Intial node: <5> or <[<1>,<1>,<1>,]>
Specification Automaton:
States: 
<1> or <[<1>,<1>,<1>,]> (initial) (final)

Transitions: 
<1> or <[<1>,<1>,<1>,]> -> <1> or <[<1>,<1>,<1>,]>: 

Creating monitor...
Shield Monitor:
States: 
<1> (final)

Transitions: 
<1> -> <1>: 

Segmentation fault (core dumped)

The issue appears to lie somewhere in the construction of the ProductDfa itself which causes all nodes to collapse into a single final node after which no shield can be created.

I created a fix/rewrite, which I could turn into a PR. I had some (local?) issues with installation though, so I had to alter the setup a bit anyway, i.e. I will need someone else to test the fix.

[florisdenhengst]

I have made a merge request based on the 'fix/rewrite' commit I linked to in the issue description.