Test if Existential Quantification works

[MClarke1991]

Around https://github.com/swoodhouse/Game/blob/b71e0ff472daea7a9f169cbc50b676030c4fee3a/src/GameDLL/GameDLL/Attractors.cpp#L325 in Attractors::attractors in src/GameDLL/GameDLL/Attractors.cpp there is an existential quantification which needs to be tested to make sure it works.

• Steven thinks that we do need to do existential quantification step, and that Nir is wrong in thinking that we don't
• Can we test whether we need this existential quantification and whether it is doing the thing we need it to do?
  • Existential quantification is needed if the when running forward from a state for n steps, you do not finish in an attractor for all mutations and all treatments
  • Currently n is set at 1000, so this is very unlikely
  • We can make a network to test this however
  • We need a case where for one case/mutation it does reach an attractor in <n steps, but for another it does not. Simplest would be a three node network, x, y, z of granularity 1500. x and y are mutation nodes, one sets z to zero, one sets z to 1500. If under the background z is 0, then when x is mutated the attractor is reached trivially. If y is mutated then z needs to reach 1500 but can only increase by 1 each step. So after n = 1000 steps it will not have reached it's attractor yet.
  • Problem might be that having such an enormous granularity runs very slowly.
  • Need to run on GAME with AND WITHOUT existential quantification to check that it fails if the Existential Quantification is not there. This is because it is not needed except in edge case, so if everything works might be that our benchmark didn't need the Existential Quantification, not that the Existential Quantification worked properly.

• [ ] Make network to test this
• [ ] Test if this network can be resolved by GAME code with EQ, and not without EQ

[MClarke1991]

Cannot have a node of granularity > 100. Instead making a chain of 11 nodes of granularity 100 for combined granularity of 1100

[MClarke1991]

And if I have nodes zi for 0<=i<=10 each must have a target function of the form `z{i+1} = min(var(z_i)-99,1)*var(z_i)`

[swoodhouse]

It's possible the check I want to do is more like

BDD variablesToKeepNonZero = (fr * br).ExistAbstract(nonPrimeVariables);
BDD frIntersected = fr * variablesToKeepNonZero;
BDD brIntersected = br * variablesToKeepNonZero;
 if ((frIntersected * !brIntersected).IsZero()) ....

I need to think about it a bit.

[MClarke1991]

Well, this network doesn't stabilise in <1000 steps (uploaded as a .txt so Github will like it) EQ_test_1_not_a_json.txt EQ_test_1_not_a_csv.txt

[swoodhouse]

Thinking aloud.. fr will always reach an attractor, for all mutation configurations. Br may = fr for some config, in which case fr is an attractor, else fr is a superset of an attractor.

What we don't want to happen is for fr for some config to be a superset of an attractor but for other configs be equal to an attractor. If this happens, fr * !br != 0 and then when we remove br we will miss these attractors and never explore them again.

[swoodhouse]

An inelegant fix would be to loop over all configs, select the fr and br for that config (fr' = fr config, and br' = br config), and check whether fr' * !br' = 0.

I was trying to do a more elegant symbolic implementation of this.

[swoodhouse]

variablesToKeepNonZero = (fr br).ExistAbstract(nonPrimeVariables) was supposed to give you all configs such that fr' !br = 0.

[swoodhouse]

configsWithAttractors = (br * !fr).ExistAbstract(nonPrimeVariables)
frIntersected = fr * configsWithAttractors
if frIntersected != 0:
  add frIntersected
S = S - s - br

[swoodhouse]

There's a much more elegant solution that I just committed - simply unroll the network until you have definitely hit an attractor in all models, rather than a constant number of steps. I'm pretty sure this resolves this issue.