The case of non-determinism is now dealt with the "old" version of the
reactant-centered model: we DON'T use the c'==0 invariant in
not_reacting, and we DO reset the clock when going from not_reacting to
updating. Moreover, I removed the self-loops in updating (those that
react to changes in upstream reactants, calling update() each time),
because I strongly suspect they are useless. The c'==0 was forcing
UPPAAL to over-approximation, which meant that exact ("normal") model
checking queries would return answers like "Property is maybe
satisfied", which is not very exact... Moreover, we did not deal
properly when parsing those answers (so now that we don't get them
anymore we are able to deal with them...? No, because the deterministic
model still has it). If we want to use the c'==0 (and not reset), we
need to set a Cytoscape network boolean property called "useOldReacting"
to false (because we assume it is true, as we currently are using the
"old" resetting approach).
We still make use of the "bigger" model (the one that waits for any
other reactant on which I depend to possibly change before I update my
time and rate calculations) when we want fully deterministic behavior:
in that case, it still makes sense to do all the work. Unfortunately, we
also have to use c'==0 in that case. Should we consider removing it, so
that we don't get "maybe" answers (but the model would not be "so much"
deterministic anymore, then..)?