search

adamtool / webinterface

The web interface for the tool Adam (AdamMC and AdamSYNT) providing an intuitive, visual definition of Petri nets with transits and Petri games, and an interactive interface to the algorithms of AdamMC and AdamSYNT. Contains the repos (as submodules): libs, framework, logics, modelchecking, examples, synthesizer, high-level, webinterface-backend.
http://adam.informatik.uni-oldenburg.de:4567/
GNU General Public License v3.0
5 stars 2 forks source link

The incrementally graph game creation does not create the whole graph #12

Closed mgieseking closed 4 years ago

mgieseking commented 4 years ago

When using the method "Calculate Graph Game BDD incrementally" the resulting graph is not the complete graph (which can be calculated with "Calculate whole Graph Game BDD").

For example: safety->burglar->burglar.apt sometimes creates in Firefox and Opera only the bad states, but Chromium does it right. buchi->mutex.apt sometimes all second states don't have any successors in Firefox and Opera, again Chromium does it right.

annyanich commented 4 years ago

I think the problem may be that if you click on graph states very quickly, it will send multiple AJAX requests to the server that are handled by separate threads in parallel. So e.g. the method "AdamSynthesizer.getSuccessors()" could be called in two separate threads for the same graphBdd / solver at the same time. I imagine that could end up with certain states getting lost as multiple threads' data structure operations are interleaved. I'm guessing your code is not meant to be called this way, right? :D (Mine neither)

I have tested it on abe and it seems promising: When I opened "Calculate Graph Game BDD Incrementally" for burglar.apt and double clicked very fast on the initial state, it ended up in a defective state, showing no successors at all, even if I clicked a third or fourth time to try to "re-expand" the state.

I will have a look at synchronizing things so that requests from a given client that operate upon a GraphBDD are handled one at a time.

annyanich commented 4 years ago

(Oops, Github automatically closed the issue based on my commit name. Reopening.)

Let me know if this handles the issue. I think that #237 from Redmine can be resolved in a similar way.

mgieseking commented 4 years ago

Seems to work for me. So far I didn't experience this bug anymore.