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

Add a visualization of whether the net satisfies the precondition #34

Open mgieseking opened 4 years ago

mgieseking commented 4 years ago

Add a tick-button to the bottom of the editor which is gray when the current net is not in a checked state and green when it is checked correctly and red otherwise.

In AdamModelChecker and AdamSynthesizer there is a method "createPreconditionChecker" which can serve for checking the net. A Petri net with transits and a Petri game with transits have a listener which notifies if s.th. structurally change in the net (see for example the implementation in "PreconditionChecker").

You can create your own listener to gray out and reactivate the button. When clicked, you can use the check method of the "PreconditionChecker" to decide whether the button is green or red. Then deactivate the button.

annyanich commented 4 years ago

@mgieseking I assign it to you while you check if its feasible to interrupt this calculation. :)

mgieseking commented 4 years ago

For getting notified if any changes in the net occur you only have to write a listener implementing IGraphListener<PetriNet, Flow, Node>, i.e., only implementing

 @Override
    public boolean changeOccurred(IGraph<PetriNet, Flow, Node> graph) {

which is triggered when the net has changed.

This listener has to be added to the Petri net with net.addListener(listener).

mgieseking commented 4 years ago

@annyanich it is feasible and I opened an issue for that #83

mgieseking commented 4 years ago

I think this was the thing we already missed for the last deadline ;).

annyanich commented 4 years ago

Recap of what I said in chat: I will probably not get around to implementing this for the deadline, so as of ab0d54bfe6320d9b92caae76f59124e7657a7f1d, the checking simply happens before each and every type of job from the solve/analyze menus. In the log window, you can see a message in the server before and after the checking takes place.

annyanich commented 4 years ago

I will put this as 3-priority for now