diff --git a/reactics-gui/resources/help/img/ctx-automaton-edge-details.png b/reactics-gui/resources/help/img/ctx-automaton-edge-details.png new file mode 100644 index 0000000..858df8e Binary files /dev/null and b/reactics-gui/resources/help/img/ctx-automaton-edge-details.png differ diff --git a/reactics-gui/resources/help/img/ctx-automaton-panel.png b/reactics-gui/resources/help/img/ctx-automaton-panel.png new file mode 100644 index 0000000..2fdd1f8 Binary files /dev/null and b/reactics-gui/resources/help/img/ctx-automaton-panel.png differ diff --git a/reactics-gui/resources/help/img/ctx-automaton-state.png b/reactics-gui/resources/help/img/ctx-automaton-state.png new file mode 100644 index 0000000..fbafe42 Binary files /dev/null and b/reactics-gui/resources/help/img/ctx-automaton-state.png differ diff --git a/reactics-gui/resources/help/img/ctx-automaton-transition-edit.png b/reactics-gui/resources/help/img/ctx-automaton-transition-edit.png new file mode 100644 index 0000000..888e93d Binary files /dev/null and b/reactics-gui/resources/help/img/ctx-automaton-transition-edit.png differ diff --git a/reactics-gui/resources/help/index.html b/reactics-gui/resources/help/index.html new file mode 100644 index 0000000..def4c4e --- /dev/null +++ b/reactics-gui/resources/help/index.html @@ -0,0 +1,265 @@ + + + + + ReactICS GUI Help + + + +
+

ReactICS - Reaction Systems Model Checker

+
+ + +

+ ReactICS is a toolkit that allows for verification of Reaction Systems. + The toolkit consists of two separate modules implementing: +

+

+

+ ReactICS GUI offers a graphical user interface allowing for editing the reaction system details + and model checking using BDD module. +

+

+ More on ReactICS can be found at The Reactics Webpage. +

+ +
+
+

Table of contents

+ +
+ + +
+

Reaction Systems

 +
+ +

+ Reaction Systems are a formalism inspired by the functioning of living cells. + They allow for specifying and analysing computational processes in which reactions operate on sets of molecules. +

+ +

+ The behaviour of a reaction system is determined by the interactions of its reactions, which are based on + the mechanisms of facilitation and inhibition. + The formal treatment of reaction systems is qualitative and there is no direct representation of the number + of molecules involved in reactions. +

+ +

+ A Distributed Reaction System is a computational model in which multiple autonomous processes (aka. agents) + interact locally through rule-based reactions. + Each agent operates independently (without any central controller—coordination), + processing inputs and producing outputs based on predefined reactions, + and their collective behavior leads to complex system dynamics. +

+ +

+ More on reaction system can be found at The Reaction System Webpage +

+ +
Back to top
+
+ +
+

Application functions

 +
+ +

+ ReactICS GUI allows to: +

+

+ +
Back to top
+ +
+ + +
+

Reaction system editor

 +
+ +

+ -- TODO -- +

+ +
Back to top
+ +
+ + +
+

Context automaton editor

 +
+ +

+ To create or edit the context automaton structure a proper edit mode should be set using the edit mode panel. +

+
+
+ +

+ The type of the newly created object (state or edge) is set by checking the proper toggle button. + With no button checked, one can transform the net by moving states around, etc. + (see below for more details). +

+ +
+ +

States

+ +

+ A new state is created by left-clicking the edit area (the main part of the component). + As it is customary in automata theory, states are numbered separately starting from 1. + The types of states are distinguished by shape and colour: + the initial state is depicted as a square, all other states are depicted as circles. + Moreover, hovering the mouse above a state allows to see its full description containing both + its name and its (distinct) number. +

+
+
+ +

+ The details of a state can be edited by right-clicking the existing + state and choosing the right option from the popup menu: +

+

+
+
+ +

Edges

+ +

+ A directed edge between two states is created by left-clicking both its endpoints in correct order. + Each edge may contain several transitions, each of them defined by a context (additional entities + provided for active processes/agents) and a guard (a condition required by the transition to execute). + The list of transitions may be edited by right-clicking the existing + edge and choosing the Nondeterministic transitions popup menu. +

+
+

+ Hovering the mouse above an edge allows to see the full list of transitions + including context and guards. +

+
+ +
+ +

Removing context automaton elements

+ +

+ Switching the toggle button Delete on allows removing context automaton elements. + Each left-clicked element is removed from the automaton grapn. + Moreover, the entire context automaton graph may be deleted by clicking the Clear button. +

+ +
+ +

Transforming the context automaton graph

+ +

+ Any state of the automaton may be picked and dragged around the edit area to obtain the desired graph shape. + It is also possible to select multiple states and move them together at the same time. + After CTRL + left-click on a particular state the entire automaton graph is shifted to be centered + on the clicked state. + Checking the Lock relative nodes positions checkbox locks the relative positions of the states. + In that case, dragging a single state moves the entire automaton graph. + Moreover, using mouse scroll the automaton graph view can be zoomed in and out. +

+ +
Back to top
+ +
+ + +
+

Transition system viewer

 +
+ +

+ The component offers the visualisation of the transition system representing the state space of the reaction systems. + The initial state is depicted as a square, all other states are depicted as circles. + There is a directed edge connecting the state Si to the state Sj + if Sf is reachable from Si by a single computation step of the reaction system. +

+ +

+ The component has two separate instances represented by two separate tabs in the application window. + The first visualises the complete state space of the reaction system, + where each state is represented by sets of entities possessed by each agent and the current context automaton state. + The second visualises the compressed state space, where context automaton states are ignored + (states are represented only by the sets of entities possessed by each agent). +

+ +

+ Computation is done by pressing Update transition system button. + The reaction system structure should be loaded from the file or edited manually for the computation to be possible. +

+ +

+ Note that no matter in which component the Update transition system button + is pressed, the transition system structure will be updated in both. +

+ +

+ Hovering the mouse above a state allows to see its full description: entities possessed by each process/agent + and the context automaton state (not present in the case of the compressed graph). +

+
+ +
+ +

Transforming the transition system graph

+ +

+ Any state of the transition system may be picked and dragged around the edit area to obtain the desired graph shape. + It is also possible to select multiple states and move them together at the same time. + After CTRL + left-click on a particular state the entire transition system graph is shifted to be centered + on the clicked state. + Checking the Lock relative nodes positions checkbox locks the relative positions of the states. + In that case, dragging a single state moves the entire transition system graph. + Moreover, using mouse scroll the transition system graph view can be zoomed in and out. +

+ +
Back to top
+ +
+ +
+

Model checking

 +
+ +

+-- TODO -- +

+ +
Back to top
+ +
+
+ + \ No newline at end of file diff --git a/reactics-gui/META-INF/MANIFEST.MF b/reactics-gui/src/META-INF/MANIFEST.MF similarity index 100% rename from reactics-gui/META-INF/MANIFEST.MF rename to reactics-gui/src/META-INF/MANIFEST.MF diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java similarity index 99% rename from reactics-gui/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java index feaa6d8..dad9e58 100644 --- a/reactics-gui/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java @@ -335,7 +335,7 @@ public class ContextAutomatonEditor extends JPanel { boolean idOk = false; do { - String newLabel = JOptionPane.showInputDialog(null, "State label", state.getLabel()); + String newLabel = JOptionPane.showInputDialog(this, "State label", state.getLabel()); if (newLabel == null) return; diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/FormulaEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java similarity index 99% rename from reactics-gui/pl/umk/mat/martinp/reactics/FormulaEditor.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java index 3b8b844..336d2db 100644 --- a/reactics-gui/pl/umk/mat/martinp/reactics/FormulaEditor.java +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java @@ -59,7 +59,7 @@ public class FormulaEditor extends JPanel { formTable.createDefaultColumnsFromModel(); setLayout(new BorderLayout()); - add(formTable, BorderLayout.CENTER); + add(new JScrollPane(formTable), BorderLayout.CENTER); } public boolean isModified() { return modified; } diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/HelpWindow.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java similarity index 97% rename from reactics-gui/pl/umk/mat/martinp/reactics/HelpWindow.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java index af917fc..ea0ca75 100644 --- a/reactics-gui/pl/umk/mat/martinp/reactics/HelpWindow.java +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java @@ -59,7 +59,7 @@ public class HelpWindow extends JFrame { JScrollPane helpScroller = new JScrollPane(); JViewport helpVp = new JViewport(); Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); - helpVp.setPreferredSize(new Dimension(screenSize.width-200, screenSize.height-200)); + helpVp.setPreferredSize(new Dimension(screenSize.width/2, screenSize.height-200)); helpVp.add(helpPane); helpScroller.setViewport(helpVp); mainPanel.add(helpScroller, BorderLayout.CENTER); diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ProcessEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/ProcessEditor.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ReactantSetPanel.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/ReactantSetPanel.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ReacticsGUI.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java similarity index 99% rename from reactics-gui/pl/umk/mat/martinp/reactics/ReacticsGUI.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java index e80f676..b2b6127 100644 --- a/reactics-gui/pl/umk/mat/martinp/reactics/ReacticsGUI.java +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java @@ -225,7 +225,7 @@ public class ReacticsGUI extends JFrame { JPanel formulaEditorPanel = new JPanel(); formulaEditorPanel.setLayout(new BorderLayout()); formulaEditor = new FormulaEditor(); - formulaEditorPanel.add(new JScrollPane(formulaEditor), BorderLayout.CENTER); + formulaEditorPanel.add(formulaEditor, BorderLayout.CENTER); JPanel formulaCtrlPanel = new JPanel(); JButton addButton = new JButton("Add formula"); @@ -311,6 +311,8 @@ public class ReacticsGUI extends JFrame { reactionSystem.clearModificationStatus(); contextAutomaton.clearModificationStatus(); formulaEditor.clearModificationStatus(); + transitionSystem.clearModificationStatus(); + compressedTransitionSystem.clearModificationStatus(); } private void updateReactionSystem() { diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ReacticsRuntime.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/ReacticsRuntime.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/TransitionEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java similarity index 100% rename from reactics-gui/pl/umk/mat/martinp/reactics/TransitionEditor.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java diff --git a/reactics-gui/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java similarity index 92% rename from reactics-gui/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java rename to reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java index cf2c290..84eca05 100644 --- a/reactics-gui/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java @@ -15,7 +15,10 @@ import javax.swing.JToolTip; import javax.swing.Icon; import javax.swing.border.EtchedBorder; import java.awt.*; +import java.util.ArrayList; import java.util.HashMap; +import java.util.regex.Matcher; +import java.util.regex.Pattern; public class TransitionSystemViewer extends JPanel { @@ -61,6 +64,8 @@ public class TransitionSystemViewer extends JPanel { // Is transition system graph already computed? boolean isComputed() { return computed; } + void clearModificationStatus() { computed = false; } + private void createGraphViever() { graphLayout = new FRLayout(tsGraph); @@ -278,6 +283,7 @@ class TSState { private final int id; private final String rsDetails; + private final String toolTipText; private final String aState; private boolean initial = false; @@ -285,12 +291,14 @@ class TSState { this.id = id; this.rsDetails = formatRSDetails(stateStr.substring(1, stateStr.length() - 1).strip()); this.aState = null; + this.toolTipText = formatToolTipText(); } public TSState(int id, String stateStr, String aState) { this.id = id; this.rsDetails = formatRSDetails(stateStr.substring(1, stateStr.length() - 1).strip()); this.aState = aState; + this.toolTipText = formatToolTipText(); } public boolean isInitial() { @@ -318,19 +326,34 @@ class TSState { } public String getTooltipText() { - if (aState != null) - return ""+ - "CA " + aState+ "
" + rsDetails + - ""; - else - return ""+ - rsDetails + - ""; + return toolTipText; } private String formatRSDetails(String rsDetails) { return rsDetails.replaceAll("\\} (proc\\d+=\\{)", "}
$1"); } + + private String formatToolTipText() { + Pattern pattern = Pattern.compile("\\w+=\\{[^}]*\\}"); + Matcher matcher = pattern.matcher(rsDetails); + + ArrayList blocks = new ArrayList(); + + while (matcher.find()) { + blocks.add(matcher.group()); + } + + if (aState != null) + return "" + + "CA " + aState+ "
" + + String.join("
", blocks) + + ""; + else + return "" + + String.join("
", blocks) + + ""; + } + }