diff --git a/reactics-bdd/export.cc b/reactics-bdd/export.cc
index 6682cec..b8fa322 100644
--- a/reactics-bdd/export.cc
+++ b/reactics-bdd/export.cc
@@ -808,3 +808,106 @@ string RSExporter::formulaToStr(const FormRSCTLK * form) {
return "??";
}
}
+
+
+void RSExporter::exportToXML() {
+ output << "\n"
+ << indent << "\n";
+
+ for (Process proc=0; procgetNumberOfProcesses(); ++proc) {
+ output << indent << indent << "processes_ids[proc] << "\">\n";
+
+ for (const auto & reaction : rs->proc_reactions[proc]) {
+ output << indent << indent << indent << "\n";
+
+ for (const Entity & e : reaction.rctt) {
+ output << indent << indent << indent << indent
+ << "" << rs->getEntityName(e) << "\n";
+ }
+
+ for (const Entity & e : reaction.inhib) {
+ output << indent << indent << indent << indent
+ << "" << rs->getEntityName(e) << "\n";
+ }
+
+ for (const Entity & e : reaction.prod) {
+ output << indent << indent << indent << indent
+ << "" << rs->getEntityName(e) << "\n";
+ }
+
+ output << indent << indent << indent << "\n";
+ }
+
+ output << indent << indent << "\n";
+ }
+
+ output << indent << "\n";
+
+ output << indent << "\n";
+
+ for (unsigned stId=0; stIdctx_aut->states_ids.size(); ++stId) {
+ if (rs->ctx_aut->states_ids[stId] == "T")
+ continue;
+
+ output << indent << indent << "ctx_aut->states_ids[stId] << "\" x=\"0\" y=\"0\"";
+
+ if (rs->ctx_aut->init_state_defined && stId == rs->ctx_aut->init_state_id)
+ output << " initial=\"true\"";
+
+ output << "/>\n";
+ }
+
+ vector>> edges(rs->ctx_aut->states_ids.size());
+
+ for (const CtxAutTransition & trans : rs->ctx_aut->transitions) {
+ if (rs->ctx_aut->states_ids[trans.src_state] == "T" || rs->ctx_aut->states_ids[trans.dst_state] == "T")
+ continue;
+
+ edges[trans.src_state][trans.dst_state].push_back(trans);
+ }
+
+ for (unsigned src=0; srcctx_aut->getStateName(src)
+ << "\" to=\"" << rs->ctx_aut->getStateName(dst.first) << "\">\n";
+
+ for (const CtxAutTransition &trans : dst.second) {
+ output << indent << indent << indent << "procEntitiesToStr(trans.ctx) << "\"";
+
+ if (trans.state_constr)
+ output << " guard=\"" << trans.state_constr->toStr() << "\"";
+
+ output << "/>\n";
+ }
+
+
+ output << indent << indent << "\n";
+ }
+ }
+
+ output << indent << "\n";
+
+ output << indent << "\n";
+
+ for (const auto & prop : drv->properties) {
+ string fStr = "";
+
+ for (const char ch : prop.second->toStr()) {
+ if (ch == '<')
+ fStr += "<";
+ else if (ch =='>')
+ fStr += ">";
+ else
+ fStr += ch;
+ }
+
+ output << indent << indent << indent << ""
+ << fStr << "\n";
+
+ }
+
+ output << indent << "\n";
+
+ output << "" << endl;
+}
diff --git a/reactics-bdd/export.hh b/reactics-bdd/export.hh
index b8b0714..bc7d3a7 100644
--- a/reactics-bdd/export.hh
+++ b/reactics-bdd/export.hh
@@ -14,6 +14,8 @@ public:
RSExporter(RctSys *rs, rsin_driver *drv, std::ostream & outStream = std::cout);
void exportToISPL();
+ void exportToXML();
+
private:
RctSys *rs;
rsin_driver *drv;
diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc
index c86fec5..90e1298 100644
--- a/reactics-bdd/reactics.cc
+++ b/reactics-bdd/reactics.cc
@@ -17,6 +17,7 @@ int main(int argc, char **argv)
bool reach_states = false;
bool reach_states_succ = false;
bool export_to_ispl = false;
+ bool export_to_xml = false;
bool bmc = true;
bool benchmarking = false;
bool dump_help_message = false;
@@ -32,7 +33,7 @@ int main(int argc, char **argv)
int c;
int option_index = 0;
- while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheEG", long_options,
+ while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheyEG", long_options,
&option_index)) != -1) {
switch (c) {
case 0:
@@ -57,6 +58,10 @@ int main(int argc, char **argv)
export_to_ispl = true;
break;
+ case 'y':
+ export_to_xml = true;
+ break;
+
//case 'b':
// printf("-b with %s\n", optarg);
// break;
@@ -141,7 +146,7 @@ int main(int argc, char **argv)
}
if (!(reach_states || reach_states_succ || rstl_model_checking
- || show_reactions || print_parsed_sys || export_to_ispl)) {
+ || show_reactions || print_parsed_sys || export_to_ispl || export_to_xml)) {
FERROR("No task specified: -c, -P, -r, -s, or -e needs to be used");
}
@@ -176,7 +181,7 @@ int main(int argc, char **argv)
rs.printSystem();
}
- if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl) {
+ if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl || export_to_xml) {
SymRS srs(&rs, opts);
ModelChecker mc(&srs, opts);
@@ -194,6 +199,11 @@ int main(int argc, char **argv)
exp.exportToISPL();
}
+ if (export_to_xml) {
+ RSExporter exp(&rs, &driver);
+ exp.exportToXML();
+ }
+
if (rstl_model_checking) {
if (bmc) {
cout << "Using BDD-based Bounded Model Checking" << endl;
@@ -269,6 +279,7 @@ void print_help(std::string path_str)
<< " -v -- verbose (use more than once to increase verbosity)" << endl
<< " -p -- show progress (where possible)" << endl
<< " -X -- backend mode (makes output parsing easier)" << endl
+ << " -y -- export to XML (for GUI tool)" << endl
<< endl
<< " Optimisations:" << endl
<< " -E -- disable auto-reordering optimisation of BDDs" << endl
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..d40c9a4
--- /dev/null
+++ b/reactics-gui/resources/help/index.html
@@ -0,0 +1,321 @@
+
+
+
+
+ ReactICS GUI Help
+
+
+
+
+ReactICS - Distributed Reaction Systems Model Checker
+
+
+
+
+ ReactICS is a toolkit that allows for verification of Reaction Systems.
+ The toolkit consists of two separate modules implementing:
+
+ - Methods using binary decision diagrams (BDD)
+ for storing and manipulating the state space of the verified system.
+ - Methods translating the verification problems into satisfiability modulo theories (SMT).
+
+
+
+ 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:
+
+ - Edit the reaction system structure (the number of processes/agents, reactions for each process/agent, etc.)
+ - Edit the context automaton structure (adding/removing states and transitions,
+ edit context for active processes/agents, setting guards for transitions, etc.).
+ - Preview of the state space represented as a transition system.
+ - Verification of properties defined by formulas using rsCTLK semantics.
+ - Save/load the reaction system structure to/from XML file.
+ - Export/import the reaction system to/from RSSL file.
+ - Export the reaction system structure and behaviour to ISPL file.
+
+
+
+Back to top
+
+
+
+
+
+Distributed reaction system editor
+
+
+
+
+ The structure of distributed reaction system can be edited using the following buttons from the distributed reaction system control panel:
+
+
+ - New process - Creates a new empty process.
+ - Remove - Removes selected processes.
+ - Copy - Makes copies of selected processes (together with all reactions).
+ - Rename - Renames a selected process. Note that process names should be unique.
+ - Move up - Moves selected process up the list of all processes.
+ - Move down - Moves selected process down the list of all processes.
+
+
+
+
+ The details of a single process can be edited using the following buttons in the process panel:
+
+
+ - Add reaction - Creates a new reaction. The details of the reaction should be specified in dialog shown below.
+ - Edit reaction - Allows to edit the details of a selected reaction using dialog shown below.
+ - Remove reaction - Removes a selected reaction.
+
+
+
+
+
+ Verification of formulas against a system specification is done after selecting desired formulas
+ and clicking Evaluate button.
+ The result of the verification (True/False), as well as time and memory used are presented next to each verified formula.
+
+
+
+ Clicking the Reset button resets the status of the model checking.
+ Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure)
+ the results of model checking, if any, are reset automatically.
+
+
+
+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:
+
+ - Set as initial - Makes the selected state the initial state of the context automaton.
+ - Set label - Allows to set the custom label for the selected state. Note that state labels have to be unique.
+
+
+
+
+
+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
+
+
+
+Model checking is handled by the component at the bottom of the application window.
+The properties of the analysed system are expressed as formulas following rsCTLK syntax.
+
+
+The list of formulas may be modified using the following buttons:
+
+ - Add formula - Creates an empty formula. The details of the formula should be specified in dialog shown below.
+ - Edit formula - Allows to edit the details of a selected formula using dialog shown below.
+ - Remove formulas - Removes selected formulas.
+
+
+
+
+
+Verification of formulas against a system specification is done after selecting desired formulas
+and clicking Evaluate button.
+The result of the verification (True/False), as well as time and memory used are presented next to each verified formula.
+
+
+
+Clicking the Reset button resets the status of the model checking.
+Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure)
+the results of model checking, if any, are reset automatically.
+
+
+Back to top
+
+
+
+
+
\ No newline at end of file
diff --git a/reactics-gui/src/META-INF/MANIFEST.MF b/reactics-gui/src/META-INF/MANIFEST.MF
new file mode 100644
index 0000000..b010a96
--- /dev/null
+++ b/reactics-gui/src/META-INF/MANIFEST.MF
@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+Main-Class: pl.umk.mat.martinp.reactics.ReacticsGUI
+
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java
new file mode 100644
index 0000000..4c1ee59
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java
@@ -0,0 +1,693 @@
+package pl.umk.mat.martinp.reactics;
+
+import edu.uci.ics.jung.algorithms.layout.FRLayout;
+import edu.uci.ics.jung.algorithms.layout.GraphElementAccessor;
+import edu.uci.ics.jung.algorithms.layout.Layout;
+import edu.uci.ics.jung.algorithms.layout.StaticLayout;
+import edu.uci.ics.jung.algorithms.layout.util.Relaxer;
+import edu.uci.ics.jung.graph.Graph;
+import edu.uci.ics.jung.graph.util.Context;
+import edu.uci.ics.jung.graph.util.Pair;
+import edu.uci.ics.jung.visualization.VisualizationViewer;
+import edu.uci.ics.jung.visualization.control.DefaultModalGraphMouse;
+import edu.uci.ics.jung.visualization.control.ModalGraphMouse;
+import edu.uci.ics.jung.visualization.decorators.EdgeShape;
+import edu.uci.ics.jung.visualization.decorators.ToStringLabeller;
+import edu.uci.ics.jung.visualization.picking.PickedState;
+import edu.uci.ics.jung.visualization.renderers.Renderer;
+import org.apache.commons.collections15.Transformer;
+import org.w3c.dom.Document;
+import javax.swing.*;
+import javax.swing.border.EtchedBorder;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.awt.event.MouseAdapter;
+import java.awt.event.MouseEvent;
+import java.awt.geom.AffineTransform;
+import java.awt.geom.Point2D;
+import java.io.PrintWriter;
+import java.util.*;
+
+
+public class ContextAutomatonEditor extends JPanel implements RSObserver {
+ private enum EditorState {STATE, EDGE, DELETE, CLEAR, NONE}
+
+ private static final long serialVersionUID = 1L;
+
+ private ReactionSystem rs;
+
+ //---------------------------------------------------------------
+ // Visual configuration settings
+ //---------------------------------------------------------------
+ private static final Color pickedNodeColor = Color.yellow;
+ //private static final Color pickedEdgeColor = Color.red;
+ private static final Color pickedEdgeColor = Color.black;
+ private static final Color edgeColor = Color.black;
+ private static final Color emptyEdgeColor = Color.lightGray;
+ private static final Font nodeLabelFont = new Font("Helvetica", Font.BOLD, 20);
+ private static final Font edgeLabelFont = new Font("Helvetica", Font.BOLD, 15);
+ private static final Font toolTipFont = new Font("Helvetica", Font.PLAIN, 14);
+ private static final float[] dash = {10.0f, 10.0f};
+ private static final Stroke basicEdgeStroke = new BasicStroke(3.0f,BasicStroke.CAP_ROUND,BasicStroke.JOIN_ROUND);
+ private static final Stroke emptyEdgeStroke = new BasicStroke(3.0f, BasicStroke.CAP_ROUND, BasicStroke.JOIN_ROUND, 10.0f, dash, 0.f);
+ private static final Stroke basicEdgeArrow = new BasicStroke(3.0f);
+ private static final Stroke emptyEdgeArrow = new BasicStroke(3.0f, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND, 10.0f, dash, 10.0f);
+
+ private static Dimension initialEditorSize;
+
+ private VisualizationViewer graphViewer;
+ private Layout gLayout;
+ DefaultModalGraphMouse graphMouse;
+ private ContextAutomatonGraph graph;
+
+ // Context menus for transitions, places and edges
+ private JPopupMenu stateContextMenu;
+ private JPopupMenu edgeContextMenu;
+ private TransitionEditor transitionEditor = null;
+
+ private EditorState edtState;
+ private Vector modeButtons;
+
+ private CAState lastPickedNode = null;
+
+
+ public ContextAutomatonEditor(Dimension size) {
+ this.setLayout(new BorderLayout());
+ initialEditorSize = size;
+
+ edtState = EditorState.NONE;
+ graph = new ContextAutomatonGraph();
+
+ createGraphEditor();
+ createModeButtonsPanel();
+ createContextMenus();
+
+ rs = ReactionSystem.getInstance();
+ }
+
+ public boolean isModified() { return graph.isModified(); }
+
+ public void clearModificationStatus() { graph.clearModificationStatus(); }
+
+ public String toRSSLString() {
+ return graph.toRSSLString();
+ }
+
+ public void exportToXML(PrintWriter output) {
+ updateNodesLocations();
+ graph.exportToXML(output);
+ }
+
+ public void loadFromXML(Document input) throws ContextAutomatonStructureError {
+ clear();
+ graph.loadFromXML(input);
+ }
+
+
+ public void recalculateCoordinates() {
+ Layout autoLayout = new FRLayout(graph, graphViewer.getSize());
+ autoLayout.initialize();
+
+ for (CAState state : graph.getVertices()) {
+ Point2D pos = autoLayout.transform(state);
+ state.updateLocation(pos);
+ }
+ }
+
+
+ public void clear() {
+ graph.clear();
+
+ for (EditorModeButton emb : modeButtons)
+ emb.setSelected(false);
+
+ graphViewer.repaint();
+ }
+
+ public void lockNodesPositions(boolean lock) {
+ if (lock)
+ graphMouse.setMode(ModalGraphMouse.Mode.TRANSFORMING);
+ else
+ graphMouse.setMode(ModalGraphMouse.Mode.PICKING);
+ }
+
+ public Set getReactantsSet() { return graph.getReactantsSet(); }
+
+ //--------------------------------------------------------------------------
+ // Creates visualization viewer for context automaton graph display/edition
+ //--------------------------------------------------------------------------
+ private void createGraphEditor() {
+ gLayout = new StaticLayout(graph,
+ new Transformer() {
+ public Point2D transform(CAState node) {
+ return node.getLocation();
+ }
+ });
+
+ graphViewer = new VisualizationViewer(gLayout, initialEditorSize) {
+ public JToolTip createToolTip() {
+ JToolTip tooltip = super.createToolTip();
+ tooltip.setFont(toolTipFont);
+ return tooltip;
+ }
+ };
+
+ // Nodes labels
+ graphViewer.getRenderContext().setVertexLabelTransformer(
+ new ToStringLabeller());
+ graphViewer.getRenderer().getVertexLabelRenderer()
+ .setPosition(Renderer.VertexLabel.Position.CNTR);
+ graphViewer.getRenderContext().setVertexFontTransformer(
+ new Transformer() {
+ public Font transform(CAState v) {
+ return nodeLabelFont;
+ }
+ });
+
+ // Nodes colour, background, etc.
+ graphViewer.getRenderContext().setVertexIconTransformer(new Transformer() {
+ public Icon transform(final CAState v) {
+ Color nodeColor = null;
+
+ if(graphViewer.getPickedVertexState().isPicked(v))
+ nodeColor = pickedNodeColor;
+ else
+ nodeColor = v.getFillColor();
+
+ return (v.isInitial() ? new SquareIcon(nodeColor, v.getWidth()) : new CircleIcon(nodeColor, v.getWidth()));
+
+ }});
+
+ // Edge color, shape and weight
+ graphViewer.getRenderContext().setEdgeDrawPaintTransformer(new Transformer() {
+ public Paint transform(CAEdge e) {
+ return edgeColor;
+ }
+ });
+
+ graphViewer.getRenderContext().setEdgeStrokeTransformer(new Transformer() {
+ public Stroke transform(CAEdge e) {
+ return basicEdgeStroke;
+ }
+ });
+
+ graphViewer.getRenderContext().setEdgeArrowStrokeTransformer(new Transformer() {
+ public Stroke transform(CAEdge e) {
+ return basicEdgeArrow;
+ }
+ });
+
+ graphViewer.getRenderContext().setArrowFillPaintTransformer(new Transformer() {
+ public Paint transform(CAEdge caEdge) {
+ if (caEdge.hasTransition())
+ return edgeColor;
+ else
+ return emptyEdgeColor;
+ }
+ });
+
+ graphViewer.getRenderContext().setEdgeShapeTransformer(new ConditionalEdgeShape<>(1.5f));
+
+ // Edge labels
+ graphViewer.getRenderContext().setEdgeLabelTransformer(new ToStringLabeller());
+ graphViewer.getRenderContext().getEdgeLabelRenderer().setRotateEdgeLabels(true);
+ graphViewer.getRenderContext().setLabelOffset(20);
+
+ graphViewer.getRenderContext().setEdgeFontTransformer(new Transformer() {
+ public Font transform(CAEdge CAEdge) {
+ return edgeLabelFont;
+ }
+ });
+
+ // For interactive graph editing
+ graphMouse = new DefaultModalGraphMouse();
+ graphViewer.setGraphMouse(graphMouse);
+
+ graphMouse.setMode(ModalGraphMouse.Mode.PICKING);
+
+ graphViewer.setVertexToolTipTransformer(new Transformer() {
+ public String transform(CAState caState) {
+ return caState.getTooltipText();
+ }
+ });
+
+ graphViewer.setEdgeToolTipTransformer(new Transformer() {
+ public String transform(CAEdge caEdge) {
+ return caEdge.getTooltipText();
+ }
+ });
+
+ graphViewer.setBackground(Color.white);
+ graphViewer.setBorder(new EtchedBorder(EtchedBorder.LOWERED));
+ graphViewer.addMouseListener(new EditorMouseListener());
+
+ add(graphViewer,BorderLayout.CENTER);
+ }
+
+ //---------------------------------------------------------------
+ // Create panel with buttons alowing editing mode choice
+ //---------------------------------------------------------------
+ private void createModeButtonsPanel() {
+ modeButtons = new Vector();
+ modeButtons.add(new EditorModeButton("STATE",new CircleIcon(CAState.baseFillColor, 15), EditorState.STATE, 0));
+ modeButtons.add(new EditorModeButton("EDGE", EditorState.EDGE, 1));
+ modeButtons.add(new EditorModeButton("DELETE", EditorState.DELETE, 2));
+ modeButtons.add(new EditorModeButton("CLEAR", EditorState.CLEAR, 3));
+
+ ModeButtonsListener mbListener = new ModeButtonsListener();
+
+ for(int i=0;i pickedVertexState = graphViewer.getPickedVertexState();
+ Set pickedNodes = pickedVertexState.getPicked();
+ Iterator it = pickedNodes.iterator();
+
+ if(!it.hasNext()) {
+ return;
+ }
+
+ CAState editedNode = it.next();
+ pickedVertexState.clear();
+
+ graph.setInitialState(editedNode);
+ }
+ });
+
+ JMenuItem setLabelItem = new JMenuItem("Set label");
+ setLabelItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent e) {
+ PickedState pickedVertexState = graphViewer.getPickedVertexState();
+ Set pickedNodes = pickedVertexState.getPicked();
+ Iterator it = pickedNodes.iterator();
+
+ if(!it.hasNext()) {
+ return;
+ }
+
+ CAState state = it.next();
+ pickedVertexState.clear();
+
+ showStateLabelEditDialog(state);
+ }
+ });
+
+ stateContextMenu.add(stateInitialItem);
+ stateContextMenu.add(setLabelItem);
+ stateContextMenu.setVisible(false);
+
+ edgeContextMenu = new JPopupMenu();
+ JMenuItem edgeLabelEditItem = new JMenuItem("Nondeterministic transitions");
+ edgeLabelEditItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent e) {
+ PickedState pickedEdgeState = graphViewer.getPickedEdgeState();
+ Set pickedEdges = pickedEdgeState.getPicked();
+ Iterator it = pickedEdges.iterator();
+
+ if(!it.hasNext()) {
+ return;
+ }
+
+ CAEdge editedEdge = it.next();
+ pickedEdgeState.clear();
+ showEdgeLabelEditDialog(editedEdge);
+ }
+ });
+
+ edgeContextMenu.add(edgeLabelEditItem);
+ edgeContextMenu.setVisible(false);
+
+ transitionEditor = new TransitionEditor();
+ }
+
+ private void showStateLabelEditDialog(CAState state) {
+ String idRegex = "[a-zA-Z][a-zA-Z_0-9:-]*";
+ boolean idOk = false;
+
+ do {
+ String newLabel = JOptionPane.showInputDialog(this, "State label", state.getLabel());
+
+ if (newLabel == null)
+ return;
+
+ newLabel = newLabel.trim();
+
+ if (!newLabel.matches(idRegex)) {
+ JOptionPane.showMessageDialog(this,
+ "State label should start with a letter and may contain only:
" +
+ "letters, numbers, colons (:), underscores (_) and hyphens (-)",
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ else {
+ idOk = true;
+ state.setLabel(newLabel);
+ }
+ }
+ while (!idOk);
+
+ graph.markAsModified();
+ this.repaint();
+ }
+
+ //---------------------------------------------------------------
+ // Creates a simple dialog window for editing edge labels
+ //---------------------------------------------------------------
+ private void showEdgeLabelEditDialog(CAEdge edge) {
+ Pair endPoints = graph.getEndpoints(edge);
+ transitionEditor.showTransitionEditDialog(this, edge.getTransitions(), endPoints.getFirst().getLabel(), endPoints.getSecond().getLabel());
+ graph.markAsModified();
+ graphViewer.repaint();
+ rs.notifyObservers();
+ }
+
+ /** Updates coordinates stored in each graph node (eg. after interactive graph modification).
+ * Called before each storing net structure to the file. */
+ private void updateNodesLocations() {
+ Collection nodes = graph.getVertices();
+
+ for(CAState n : nodes) {
+ n.updateLocation(gLayout.transform(n));
+ }
+ }
+
+ /** For better vertex placement */
+ private void relax() {
+ Layout layout = graphViewer.getGraphLayout();
+ layout.initialize();
+ layout.setSize(graphViewer.getSize());
+ Relaxer relaxer = graphViewer.getModel().getRelaxer();
+ if (relaxer != null) {
+ relaxer.stop();
+ relaxer.prerelax();
+ relaxer.relax();
+ }
+ }
+
+ public void onRSUpdate() {
+ repaint();
+ }
+
+ //---------------------------------------------------------------------------------------------
+
+
+ static class EditorModeButton extends JToggleButton {
+ private EditorState mode;
+ int seqNum;
+
+ public EditorModeButton(String label, EditorState mode) {
+ super(label);
+
+ this.mode = mode;
+ seqNum = 0;
+ }
+
+ public EditorModeButton(String label, EditorState mode, int seqNum) {
+ super(label);
+
+ this.mode = mode;
+ this.seqNum = seqNum;
+ }
+
+ public EditorModeButton(String label, Icon icon, EditorState mode, int seqNum) {
+ super(label, icon);
+
+ this.mode = mode;
+ this.seqNum = seqNum;
+ }
+
+ public EditorState getMode() {
+ return mode;
+ }
+
+ public int getSeqNum() {
+ return seqNum;
+ }
+ }
+
+
+ //---------------------------------------------------------------------------------------------
+
+
+ class ModeButtonsListener implements ActionListener {
+
+ public void actionPerformed(ActionEvent changeEvent) {
+ EditorModeButton emb = (EditorModeButton) changeEvent.getSource();
+
+ if(emb.isSelected()) {
+ int num = emb.getSeqNum();
+
+ for(int i=0;i pickSupport = null;
+ Layout layout = null;
+ CAState node = null;
+ CAEdge edge = null;
+
+ switch(edtState) {
+ case STATE:
+ try {
+ // Transform screen coordinates to layout coordinates.
+ // Necessary for possible automaton structure viewer scaling.
+ Point2D nodeLocation = graphViewer.getRenderContext().getMultiLayerTransformer().inverseTransform(clickPt);
+ graph.addState(new CAState(nodeLocation));
+ } catch (ContextAutomatonStructureError e) {
+ JOptionPane.showMessageDialog(null,
+ e.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ break;
+
+ case EDGE:
+ PickedState pickedVertexState = graphViewer.getPickedVertexState();
+
+ pickSupport = graphViewer.getPickSupport();
+ layout = graphViewer.getGraphLayout();
+ node = pickSupport.getVertex(layout, clickPt.getX(), clickPt.getY());
+
+ if (node != null) {
+ if (lastPickedNode == null) {
+ lastPickedNode = node;
+ } else {
+ graph.addEdge(lastPickedNode, node);
+ lastPickedNode = null;
+ pickedVertexState.pick(node,false);
+ }
+ } else {
+ lastPickedNode = null;
+ }
+
+ break;
+
+ case DELETE:
+ pickSupport = graphViewer.getPickSupport();
+ layout = graphViewer.getGraphLayout();
+ node = pickSupport.getVertex(layout, clickPt.getX(), clickPt.getY());
+ edge = pickSupport.getEdge(layout, clickPt.getX(), clickPt.getY());
+
+ if (node != null) {
+ Collection edges = graph.getIncidentEdges(node);
+
+ for (CAEdge e : edges)
+ rs.removeCAEdge(e);
+
+ graph.removeState(node);
+ }
+ else if (edge != null) {
+ graph.removeEdge(edge);
+ rs.removeCAEdge(edge);
+ }
+
+ break;
+
+ case NONE:
+ default:
+ break;
+ }
+
+ me.consume();
+ }
+
+ private void rightButtonClicked(MouseEvent me) {
+ GraphElementAccessor pickSupport = graphViewer.getPickSupport();
+ Layout layout = graphViewer.getGraphLayout();
+ CAState node = pickSupport.getVertex(layout, me.getX(), me.getY());
+ CAEdge edge = pickSupport.getEdge(layout, me.getX(), me.getY());
+
+ if (node != null) {
+ PickedState pickedVertexState = graphViewer.getPickedVertexState();
+ pickedVertexState.clear();
+ pickedVertexState.pick(node,true);
+ stateContextMenu.show(graphViewer, me.getX(), me.getY());
+ }
+ else if (edge != null) {
+ PickedState pickedEdgeState = graphViewer.getPickedEdgeState();
+ pickedEdgeState.clear();
+ pickedEdgeState.pick(edge, true);
+ edgeContextMenu.show(graphViewer, me.getX(), me.getY());
+ }
+
+ me.consume();
+ }
+
+ };
+
+ //---------------------------------------------------------------------------------------------
+ // For drawing the initial state
+ //---------------------------------------------------------------------------------------------
+
+ static class SquareIcon implements Icon {
+ private Color fillColor;
+ private int width;
+
+ public SquareIcon(Color fColor, int width) {
+ fillColor = fColor;
+ this.width = width;
+ }
+
+ public void paintIcon(Component c, Graphics g, int x, int y) {
+ g.setColor(fillColor);
+ g.fillRect(x, y, width, width);
+ g.setColor(Color.black);
+ g.drawRect(x, y, width, width);
+ }
+
+ public int getIconWidth() {
+ return width;
+ }
+
+ public int getIconHeight() {
+ return width;
+ }
+ }
+
+ //---------------------------------------------------------------------------------------------
+ // For drawing all non-initial states
+ //---------------------------------------------------------------------------------------------
+
+ static class CircleIcon implements Icon {
+ private Color fillColor;
+ private int radius;
+
+ public CircleIcon(Color fColor, int radius) {
+ fillColor = fColor;
+ this.radius = radius;
+ }
+
+ public void paintIcon(Component c, Graphics g, int x, int y) {
+ g.setColor(fillColor);
+ g.fillOval(x, y, radius, radius);
+ g.setColor(Color.black);
+ g.drawOval(x, y, radius, radius);
+ }
+
+ public int getIconWidth() {
+ return radius;
+ }
+
+ public int getIconHeight() {
+ return radius;
+ }
+
+ }
+
+}
+
+
+class ConditionalEdgeShape implements Transformer, E>, Shape> {
+
+ private final EdgeShape.Loop loopShape;
+ private final Transformer, E>, Shape> defaultShape;
+ private final float loopScale;
+
+ public ConditionalEdgeShape(float loopScale) {
+ this.loopShape = new EdgeShape.Loop<>();
+ this.defaultShape = new EdgeShape.QuadCurve<>(); // or Line<>
+ this.loopScale = loopScale;
+ }
+
+ public Shape transform(Context, E> context) {
+ Graph graph = context.graph;
+ E edge = context.element;
+ V src = graph.getSource(edge);
+ V dst = graph.getDest(edge);
+
+ if (src.equals(dst)) {
+ // Scale the self-loop
+ Shape baseLoop = loopShape.transform(context);
+
+ Rectangle bounds = baseLoop.getBounds();
+ double centerX = bounds.getCenterX();
+ double centerY = bounds.getCenterY();
+
+ AffineTransform at = new AffineTransform();
+ at.translate(centerX, centerY);
+ at.scale(loopScale, loopScale);
+ at.translate(-centerX, -centerY);
+
+ return at.createTransformedShape(baseLoop);
+ } else {
+ return defaultShape.transform(context);
+ }
+ }
+}
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java
new file mode 100644
index 0000000..ffd3305
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java
@@ -0,0 +1,438 @@
+package pl.umk.mat.martinp.reactics;
+
+
+import edu.uci.ics.jung.graph.DirectedSparseGraph;
+import edu.uci.ics.jung.graph.util.Pair;
+import org.w3c.dom.Document;
+import org.w3c.dom.Element;
+import org.w3c.dom.Node;
+import org.w3c.dom.NodeList;
+import java.awt.*;
+import java.awt.geom.Point2D;
+import java.io.PrintWriter;
+import java.util.*;
+
+
+class ContextAutomatonGraph extends DirectedSparseGraph {
+ private static final long serialVersionUID = 1L;
+
+ HashMap states = new HashMap<>();
+ private CAState initialState = null;
+ boolean modified = false;
+
+ public ContextAutomatonGraph() {
+ super();
+ }
+
+ public boolean isModified() { return modified; }
+
+ public void markAsModified() { modified = true; }
+
+ public void clearModificationStatus() { modified = false; }
+
+ String toRSSLString() {
+ StringBuilder rsslString = new StringBuilder("context-automaton {\n");
+
+ rsslString.append(" states { ");
+ Collection allStates = states.values();
+ Iterator it = allStates.iterator();
+ if (it.hasNext()) {
+ rsslString.append(it.next().getLabel());
+ }
+ while (it.hasNext()) {
+ rsslString.append(", ").append(it.next().getLabel());
+ }
+ rsslString.append(" };\n");
+
+ rsslString.append(" init-state { ").append(initialState != null ? initialState.getLabel() : "").append(" };\n");
+ rsslString.append(" transitions {\n");
+
+ for (CAEdge edge : this.getEdges()) {
+ for (Transition tr : edge.getTransitions()) {
+ rsslString.append(" { ").append(tr.context).append(" }: ");
+ rsslString.append(this.getSource(edge).label).append(" -> ").append(this.getDest(edge).label);
+
+ String guard = tr.guard;
+
+ if (guard.length() > 0) {
+ rsslString.append(" : ").append(guard);
+ }
+
+ rsslString.append(";\n");
+ }
+ }
+ rsslString.append(" };\n");
+
+ rsslString.append("};\n");
+
+ return rsslString.toString();
+ }
+
+ public void exportToXML(PrintWriter output) {
+ output.println(" ");
+
+ for (CAState state : states.values()) {
+ Point2D pos = state.getLocation();
+ output.print(" ");
+ }
+
+ for (CAEdge edge : edges.keySet()) {
+ Pair endPts = this.getEndpoints(edge);
+ output.print(" ");
+
+ for (Transition tr : edge.getTransitions()) {
+ output.print(" ");
+ }
+ output.println(" ");
+ }
+
+ output.println(" ");
+ }
+
+ /**
+ * Reads the context automaton structure from the XML file.
+ *
+ * @param input An XML file containing a valid description of a context automaton.
+ * @throws ContextAutomatonStructureError In the case of inputFile structure error, eg. \
+ * more than one context-automaton section, more than one \
+ * initial state, repeating state identifiers, \
+ * edge between non-existing nodes, etc.
+ */
+ public void loadFromXML(Document input) throws ContextAutomatonStructureError {
+ NodeList caSections = input.getElementsByTagName("context-automaton");
+
+ if (caSections.getLength() == 0 || caSections.getLength() > 1) {
+ throw new ContextAutomatonStructureError("An XML file should contain a single context automaton description.");
+ }
+
+ //--------------------------------------------------------------------------------------------------------------
+ // Retrieve the states
+ //--------------------------------------------------------------------------------------------------------------
+
+ HashMap states = new HashMap();
+ NodeList stateList = input.getElementsByTagName("state");
+ boolean hasInitialState = false;
+
+ for (int idx = 0; idx < stateList.getLength(); ++idx) {
+ Node stateNode = stateList.item(idx);
+
+ if (stateNode.getNodeType() != Node.ELEMENT_NODE) {
+ continue;
+ }
+
+ Element stateElement = (Element) stateNode;
+
+ int id = Integer.parseInt(stateElement.getAttribute("id"));
+ double x = Double.parseDouble(stateElement.getAttribute("x"));
+ double y = Double.parseDouble(stateElement.getAttribute("y"));
+ String name = stateElement.getAttribute("name");
+ String initial = stateElement.getAttribute("initial");
+
+ if (states.containsKey(name)) {
+ throw new ContextAutomatonStructureError("State name <" + name + "> already used.");
+ }
+
+ CAState newState = new CAState(id, name, new Point2D.Double(x, y));
+ this.addState(newState);
+ states.put(name, newState);
+
+ if (initial.equals("true")) {
+ if (hasInitialState)
+ throw new ContextAutomatonStructureError("There should not be more than one initial state.");
+
+ hasInitialState = true;
+ this.setInitialState(newState);
+ }
+ }
+
+ //--------------------------------------------------------------------------------------------------------------
+ // Retrieve the edges
+ //--------------------------------------------------------------------------------------------------------------
+
+ NodeList edgeList = input.getElementsByTagName("edge");
+
+ for (int idx = 0; idx < edgeList.getLength(); ++idx) {
+ Node edgeNode = edgeList.item(idx);
+
+ if (edgeNode.getNodeType() != Node.ELEMENT_NODE) {
+ continue;
+ }
+
+ Element edgeElement = (Element) edgeNode;
+
+ String from = edgeElement.getAttribute("from");
+ String to = edgeElement.getAttribute("to");
+
+ // Retrieve all child nodes describing nondeterministic transitions related to this edge
+ NodeList childNodeList = edgeNode.getChildNodes();
+ Vector transitionList = new Vector();
+
+ for (int cIdx=0; cIdx < childNodeList.getLength(); ++ cIdx) {
+ Node childNode = childNodeList.item(cIdx);
+
+ if (childNode.getNodeType() != Node.ELEMENT_NODE) {
+ continue;
+ }
+
+ Element transElement = (Element) childNode;
+ transitionList.add(new Transition(transElement.getAttribute("context"), transElement.getAttribute("guard")));
+ }
+
+ CAState stateFrom = states.get(from);
+ CAState stateTo = states.get(to);
+
+ if (stateFrom == null || stateTo == null)
+ throw new ContextAutomatonStructureError("An edge may be created only between existing nodes.");
+
+ this.addEdge(stateFrom, stateTo, transitionList);
+ }
+ }
+
+ public Set getReactantsSet() {
+ Set reactants = new HashSet();
+
+ for (CAEdge edge : getEdges()) {
+ for (Transition trans : edge.getTransitions()) {
+ int start = trans.context.indexOf("{");
+ int end = trans.context.indexOf("}");
+
+ if (start != -1 && end != -1 && start < end) {
+ reactants.addAll(Arrays.asList(trans.context.substring(start + 1, end).split("\\s*,\\s*")));
+ }
+ }
+ }
+
+ return reactants;
+ }
+
+ public void setInitialState(CAState state) {
+ if (initialState != null)
+ initialState.setInitial(false);
+
+ state.setInitial(true);
+ initialState = state;
+ modified = true;
+ }
+
+ public CAState getInitialState() {
+ return initialState;
+ }
+
+ /**
+ * Clears the entire automaton structure structure
+ */
+ public void clear() {
+ for (CAState st : states.values())
+ removeVertex(st);
+
+ states.clear();
+ CAState.resetIdCounter();
+ modified = true;
+ }
+
+ public boolean addEdge(CAState from, CAState to) {
+ modified = true;
+
+ return this.addEdge(new CAEdge(), from, to);
+ }
+
+ public void addEdge(CAState from, CAState to, Collection transitionList) {
+ CAEdge edge = this.findEdge(from, to);
+
+ if (edge == null) {
+ CAEdge caEdge = ReactionSystem.getInstance().createCAEdge();
+ caEdge.addTransitions(transitionList);
+ this.addEdge(caEdge, from, to);
+ }
+ else
+ edge.addTransitions(transitionList);
+
+ modified = true;
+ }
+
+ public void addState(CAState state) throws ContextAutomatonStructureError {
+ int stateId = state.getId();
+
+ if (states.get(stateId) != null)
+ throw new ContextAutomatonStructureError("State id " + stateId + " already in use.");
+
+ states.put(stateId, state);
+ this.addVertex(state);
+ modified = true;
+ }
+
+ public boolean removeState(CAState state) {
+ if (states.get(state.getId()) != null) {
+ states.remove(state.getId());
+ }
+
+ modified = true;
+
+ // Remove the state with all connected edges
+ return this.removeVertex(state);
+ }
+
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Single node of the context automaton graph
+//-------------------------------------------------------------------------------------------------
+
+class CAState {
+ public final static Color baseFillColor = Color.lightGray;
+ public final static Color selectedFillColor = Color.lightGray;
+ public final static Color initStateFillColor = new Color(102, 178, 255);
+
+ private static final int nodeWidth = 30;
+ private static final int nodeHeight = 30;
+ protected static int nextId = 1;
+
+ /** Unique auto incremented identifier of the node */
+ protected int id;
+
+ /** User defined label of the node displayed as a tool tip and used in RSSL and XML files */
+ protected String label;
+
+ protected Point2D location;
+ private boolean isInitial = false;
+
+ /** A state created from the description stored in a file. */
+ public CAState(int id, String label, Point2D location) {
+ this.id = id;
+ this.label = label;
+ this.location = location;
+
+ // To avoid duplicate node identifiers
+ if (id >= nextId)
+ nextId = id + 1;
+ }
+
+ /** A state created by clicking in graphical component. */
+ public CAState(Point2D location) {
+ this.id = nextId;
+ this.label = "q" + id;
+ this.location = location;
+ ++nextId;
+ }
+
+ public Point2D getLocation() { return location; }
+ public void updateLocation(Point2D location) { this.location = location; }
+
+ public boolean isInitial() { return isInitial; }
+ public void setInitial(boolean status) { isInitial = status; }
+
+ public int getWidth() { return nodeWidth; }
+ public int getHeight() { return nodeHeight; }
+
+ public String getLabel() { return label; }
+ public void setLabel(String newLabel) { label = newLabel; }
+
+ public int getId() { return id; }
+
+ static void resetIdCounter() { nextId = 1; }
+
+ public String toString() { return Integer.toString(id); }
+
+ public String getTooltipText() {
+ return ""+
+ "State " + id + "
" + getLabel() + //"
"+
+ "";
+ }
+
+ Color getFillColor() {
+ return isInitial ? initStateFillColor : baseFillColor;
+ }
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Single edge of the context automaton graph.
+// Each edge can represent a number of single transitions between the same pair of automaton states.
+//-------------------------------------------------------------------------------------------------
+
+class CAEdge {
+ protected static int nextId = 0;
+
+ protected int id;
+
+ // The list of all nondeterministic transitions represented by this edge
+ private Vector transitions = new Vector();
+
+ public boolean hasTransition() { return transitions.size() > 0; }
+
+
+ public CAEdge() {
+ this.id = nextId++;
+ }
+
+// public CAEdge(Collection transitionList) {
+// this.transitions.addAll(transitionList);
+// }
+
+ Vector getTransitions() {
+ return transitions;
+ }
+
+ public int getId() {
+ return id;
+ }
+
+ public String toString() {
+ // Update this if you need any label displayed together with graph edge
+ return "";
+ }
+
+ public String getTooltipText() {
+ StringBuilder tooTip = new StringBuilder("
Context : Guard
");
+
+ for (Transition tr : transitions) {
+ tooTip.append(tr.context).append(" : ").append(tr.guard).append("
");
+ }
+
+ tooTip.append("");
+
+ return tooTip.toString();
+ }
+
+ public void addTransitions(Collection transitionList) {
+ transitions.addAll(transitionList);
+ }
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Single transition. To be included in a multiedge.
+//-------------------------------------------------------------------------------------------------
+
+class Transition {
+ String context;
+ String guard;
+
+ public Transition(String ctx, String grd) {
+ context = ctx;
+ guard = grd;
+ }
+}
+
+
+class ContextAutomatonStructureError extends FileStructureError {
+ public ContextAutomatonStructureError(String message) {
+ super(message);
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java
new file mode 100644
index 0000000..0b32f30
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java
@@ -0,0 +1,13 @@
+package pl.umk.mat.martinp.reactics;
+
+import javax.swing.*;
+import java.awt.*;
+
+public class CumulatedReactionsViewer extends JPanel {
+
+ public CumulatedReactionsViewer() {
+ this.setLayout(new BorderLayout());
+ this.add(new JLabel("Cumulate Reactions Viewer", SwingConstants.CENTER), BorderLayout.CENTER);
+ }
+
+}
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java
new file mode 100644
index 0000000..9ce60e6
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java
@@ -0,0 +1,410 @@
+package pl.umk.mat.martinp.reactics;
+
+import org.w3c.dom.Document;
+import org.w3c.dom.Element;
+import org.w3c.dom.Node;
+import org.w3c.dom.NodeList;
+
+import javax.swing.*;
+import javax.swing.border.Border;
+import javax.swing.border.EtchedBorder;
+import javax.swing.event.TableModelEvent;
+import javax.swing.event.TableModelListener;
+import javax.swing.table.*;
+import java.awt.*;
+import java.io.*;
+import java.util.Collection;
+import java.util.Vector;
+
+
+public class FormulaEditor extends JPanel implements RSObserver {
+ private FormulaTableModel ftModel;
+ private JTable formTable;
+ private ReactionSystem rs;
+ private Vector formulaList;
+
+ boolean modified = false;
+
+ static final Color TableHeaderBackgroundColor = Color.gray;
+ static final Color TableHeaderFontColor = Color.white;
+ static final Color BaseFormulaBackgroundColor = Color.white;
+ static final Color TrueFormulaBackgroundColor = new Color(138, 242, 183);
+ static final Color FalseFormulaBackgroundColor = new Color(240, 141, 141);
+ static final Color InvalidFormulaBackgroundColor = new Color(124, 124, 124);
+ static final Border emptyBorder = BorderFactory.createEmptyBorder(1, 1, 1, 1);
+ static final Border selectedBorder = BorderFactory.createLineBorder(Color.RED, 2);
+
+
+ public FormulaEditor(ReactionSystem rs) {
+ this.rs = rs;
+ formulaList = rs.formulas;
+
+ // Create the table for displaying formulas. Prevent default selection modes.
+ ftModel = new FormulaTableModel();
+ formTable = new JTable(ftModel, new FormulaColumnModel());
+ formTable.setCellSelectionEnabled(false);
+ formTable.setRowSelectionAllowed(true);
+
+ Font headerFont = formTable.getTableHeader().getFont();
+ Font cellFont = formTable.getFont();
+ JTableHeader formHeader = formTable.getTableHeader();
+ formTable.setFont(new Font("Monospaced", Font.PLAIN, cellFont.getSize() + 2));
+ formHeader.setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2));
+ formHeader.setBackground(TableHeaderBackgroundColor);
+ formHeader.setForeground(TableHeaderFontColor);
+ formHeader.setReorderingAllowed(false);
+ formHeader.setResizingAllowed(true);
+ formHeader.setBorder(new EtchedBorder(EtchedBorder.LOWERED));
+
+ FormulaTableCellRenderer renderer = new FormulaTableCellRenderer();
+ formTable.setDefaultRenderer(Object.class, renderer);
+ formTable.createDefaultColumnsFromModel();
+
+ setLayout(new BorderLayout());
+ add(new JScrollPane(formTable), BorderLayout.CENTER);
+ }
+
+ public boolean isModified() { return modified; }
+
+ public void clearModificationStatus() { modified = false; }
+
+ public String toRSSLString() {
+ StringBuilder rsslString = new StringBuilder();
+
+ for (Formula f: formulaList)
+ rsslString.append(f.toRSSLString()).append("\n");
+
+ return rsslString.toString();
+ }
+
+ public void exportToXML(PrintWriter output) {
+ output.println(" ");
+
+ for (Formula f : formulaList)
+ output.println(" " + f.toXMLString());
+
+ output.println(" ");
+ }
+
+ public void loadFromXML(Document input) {
+ formulaList.clear();
+
+ NodeList formulaTags = input.getElementsByTagName("formula");
+
+ for (int idx = 0; idx < formulaTags.getLength(); ++idx) {
+ Node formulaNode = formulaTags.item(idx);
+
+ if (formulaNode.getNodeType() != Node.ELEMENT_NODE) {
+ continue;
+ }
+
+ Element formulaElement = (Element) formulaNode;
+
+ String label = formulaElement.getAttribute("label");
+ String formula = formulaElement.getTextContent();
+ formulaList.add(new Formula(label, formula));
+ }
+
+ ftModel.fireTableDataChanged();
+ }
+
+ private boolean showFormulaEditDialog(JFrame parent, Formula ff) {
+ final int Select = 0;
+ final int Approve = 1;
+
+ JTextField labelInput = new JTextField(30);
+ JTextField formulaInput = new JTextField(30);
+
+ String labelStr = "";
+ String formulaStr = "";
+
+ labelStr = ff.label;
+ formulaStr = ff.formula;
+
+ labelInput.setToolTipText("A unique label of the formula");
+ formulaInput.setToolTipText("Formula to be evaluated");
+
+ JPanel myPanel = new JPanel(new GridBagLayout());
+ GridBagConstraints cs = new GridBagConstraints();
+
+ cs.insets = new Insets(5, 5, 5, 5);
+ cs.anchor = GridBagConstraints.WEST;
+ cs.gridx = 0;
+ cs.gridy = 0;
+ myPanel.add(new JLabel("Label"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 0;
+ myPanel.add(labelInput, cs);
+
+ cs.gridx = 0;
+ cs.gridy = 1;
+ myPanel.add(new JLabel("Formula"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 1;
+ myPanel.add(formulaInput, cs);
+
+ int opStatus = Select;
+
+ do {
+ labelInput.setText(labelStr);
+ formulaInput.setText(formulaStr);
+
+ int result = JOptionPane.showConfirmDialog(parent, myPanel,
+ "Formula details", JOptionPane.OK_CANCEL_OPTION);
+
+ if (result != JOptionPane.OK_OPTION) {
+ return false;
+ }
+
+ labelStr = labelInput.getText();
+ formulaStr = formulaInput.getText();
+
+ ff.label = labelStr;
+ ff.formula = formulaStr;
+
+ opStatus = Approve;
+ }
+ while(opStatus == Select);
+
+ return true;
+ }
+
+ public void addFormula(JFrame parent) {
+ Formula ff = new Formula();
+
+ if (showFormulaEditDialog(parent, ff)) {
+ formulaList.add(ff);
+ modified = true;
+ ftModel.fireTableDataChanged();
+ }
+ }
+
+ // If more than one formula is selected throw an exception only the first can be edited
+ public void editFormula(JFrame parent) {
+ int[] selected = formTable.getSelectedRows();
+
+ if (selected.length != 1) {
+ JOptionPane.showMessageDialog(parent, "Select a single formula to edit.", "Select formula", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ Formula fEdt = formulaList.get(formTable.convertRowIndexToModel(selected[0]));
+
+ if (fEdt == null)
+ return;
+
+ showFormulaEditDialog(parent, fEdt);
+ fEdt.status = Formula.FormulaStatus.None;
+ modified = true;
+ ftModel.fireTableDataChanged();
+ }
+
+ public void removeFormulas() {
+ int[] viewRows = formTable.getSelectedRows();
+
+ // Remove formulas starting from the last to avoid indexes updates
+ for (int vIdx = viewRows.length - 1; vIdx>=0; --vIdx) {
+ int mr = formTable.convertRowIndexToModel(viewRows[vIdx]);
+ formulaList.remove(mr);
+ }
+
+ modified = true;
+ ftModel.fireTableDataChanged();
+ }
+
+ public Collection getSelectedFormulas() {
+ Vector selected = new Vector();
+ int[] viewRows = formTable.getSelectedRows();
+
+ for (int vr : viewRows) {
+ int mr = formTable.convertRowIndexToModel(vr);
+ selected.add(formulaList.get(mr));
+ }
+
+ return selected;
+ }
+
+ // Needed to repaint JTable. Called after content modification by an external object.
+ public void refreshStatus() {
+ ftModel.fireTableDataChanged();
+ }
+
+ public void resetFormulasStatus() {
+ for (Formula ff : formulaList) {
+ ff.status = Formula.FormulaStatus.None;
+ ff.mcTime = ff.totalTime = ff.memory = "-";
+ }
+
+ ftModel.fireTableDataChanged();
+ }
+
+ public void onRSUpdate() {
+ resetFormulasStatus();
+ refreshStatus();
+ }
+
+ static class FormulaColumnModel extends DefaultTableColumnModel {
+ int colno = 0;
+
+ public void addColumn(TableColumn tc) {
+ switch (colno) {
+ case 0 -> {
+ tc.setMinWidth(60);
+ tc.setMaxWidth(Integer.MAX_VALUE / 10);
+ tc.setPreferredWidth(100);
+ }
+ case 1 -> {
+ tc.setMinWidth(100);
+ tc.setMaxWidth(Integer.MAX_VALUE);
+ }
+ case 2, 3, 4, 5 -> {
+ tc.setMinWidth(50);
+ tc.setPreferredWidth(50);
+ tc.setMaxWidth(Integer.MAX_VALUE / 10);
+ }
+ }
+
+ super.addColumn(tc);
+ ++colno;
+ }
+ }
+
+
+ class FormulaTableModel extends AbstractTableModel implements TableModelListener {
+ private final String[] columnNames = {"Label", "Formula", "Status", "MC Time (s)", "Total Time (s)", "Memory (MB)"};
+
+ public String getColumnName(int colIdx) {
+ return columnNames[colIdx];
+ }
+
+ public int getRowCount() {
+ return formulaList.size();
+ }
+
+ public int getColumnCount() {
+ return columnNames.length;
+ }
+
+ public Object getValueAt(int row, int column) {
+ Formula ff = formulaList.get(row);
+
+ return switch (column) {
+ case 0 -> ff.label;
+ case 1 -> ff.formula;
+ case 2 -> ff.status;
+ case 3 -> ff.mcTime;
+ case 4 -> ff.totalTime;
+ case 5 -> ff.memory;
+ default -> "";
+ };
+ }
+
+ public void setValueAt(Object value, int row, int column) {
+// fireTableDataChanged();
+ }
+
+ public boolean isCellEditable(int rowIndex, int columnIndex) { return false; }
+
+ public Class getColumnClass(int column) {
+ return getValueAt(0, column).getClass();
+ }
+
+ public void tableChanged(TableModelEvent tableModelEvent) { }
+ }
+
+
+ // To properly display the content of the table containing formulas
+ class FormulaTableCellRenderer extends JLabel implements TableCellRenderer {
+
+ public FormulaTableCellRenderer() {
+ // Allows background to be visible
+ setOpaque(true);
+ }
+
+ public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) {
+ String statusStr = "";
+ Formula ff = formulaList.get(row);
+
+ setForeground(Color.black);
+
+ if (isSelected) {
+ setBorder(selectedBorder);
+ }
+ else {
+ setBorder(emptyBorder);
+ }
+
+ // Set cell background and formula evaluation status
+ if (column == 2) {
+ switch (ff.status) {
+ case None -> {
+ statusStr = "?";
+ setBackground(BaseFormulaBackgroundColor);
+ }
+ case True -> {
+ statusStr = "True";
+ setBackground(TrueFormulaBackgroundColor);
+ }
+ case False -> {
+ statusStr = "False";
+ setBackground(FalseFormulaBackgroundColor);
+ }
+ case Invalid -> {
+ statusStr = "Invalid";
+ setBackground(InvalidFormulaBackgroundColor);
+ }
+ }
+
+ setText(statusStr);
+ }
+ else {
+ setText((String) value);
+ setBackground(BaseFormulaBackgroundColor);
+ }
+
+ if (column > 2) {
+ setHorizontalAlignment(SwingConstants.RIGHT);
+ } else {
+ setHorizontalAlignment(SwingConstants.LEFT);
+ }
+
+ return this;
+ }
+ }
+}
+
+
+class Formula {
+ public enum FormulaStatus {None, True, False, Invalid};
+
+ String label;
+ String formula;
+ FormulaStatus status;
+ String mcTime;
+ String totalTime;
+ String memory;
+
+ public Formula() {
+ this("", "");
+ }
+
+ public Formula(String label, String formula) {
+ this.label = label;
+ this.formula = formula;
+ this.status = FormulaStatus.None;
+ this.mcTime = this.totalTime = this.memory = "-";
+ }
+
+ public String toRSSLString() {
+ return "rsctlk-property { " + label + " : " + formula + " };";
+ }
+
+ public String toXMLString() {
+ return "" +
+ formula.replaceAll("<", "<").replaceAll(">", ">") +
+ "";
+ }
+}
+
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java
new file mode 100644
index 0000000..9e970cf
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java
@@ -0,0 +1,125 @@
+package pl.umk.mat.martinp.reactics;
+
+import javax.swing.*;
+import javax.swing.border.*;
+import javax.swing.event.*;
+import java.awt.*;
+import java.awt.event.*;
+import java.net.*;
+
+public class HelpWindow extends JFrame {
+ private static final long serialVersionUID = 327019113533268901L;
+ private static final String startDocument = "index.html";
+ private static final String docPath = "/help/";
+
+ private static HelpWindow instance = null;
+ private static JTextPane helpPane = new JTextPane();;
+
+ public static synchronized HelpWindow getInstance() {
+ if (instance == null)
+ instance = new HelpWindow();
+
+ return instance;
+ }
+
+ private HelpWindow() {
+ super("ReactICS GUI Help");
+
+ getContentPane().setLayout(new BorderLayout());
+
+ JPanel mainPanel = new JPanel();
+ mainPanel.setLayout(new BorderLayout());
+ EtchedBorder panelBorder = new EtchedBorder(EtchedBorder.LOWERED);
+ mainPanel.setBorder(panelBorder);
+
+ helpPane.setEditable(false);
+ helpPane.addHyperlinkListener(new HyperlinkListener() {
+ public void hyperlinkUpdate(HyperlinkEvent hle) {
+ if (hle.getEventType() == HyperlinkEvent.EventType.ACTIVATED) {
+ String target = hle.getDescription();
+
+ if (target.startsWith("#")) {
+ helpPane.scrollToReference(target.substring(1));
+ }
+ }
+ }
+ });
+
+ try {
+ URL helpUrl = this.getClass().getResource(docPath + startDocument);
+ helpPane.setPage(helpUrl);
+
+ helpPane.revalidate();
+ helpPane.repaint();
+ }
+ catch (Exception e) {
+ System.out.println("Exception: " + e.getMessage());
+ JOptionPane.showMessageDialog(null, "Can not load help content",
+ "Help", JOptionPane.ERROR_MESSAGE);
+ }
+
+ JScrollPane helpScroller = new JScrollPane();
+ JViewport helpVp = new JViewport();
+ Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
+ helpVp.setPreferredSize(new Dimension(screenSize.width/2, screenSize.height-200));
+ helpVp.add(helpPane);
+ helpScroller.setViewport(helpVp);
+ mainPanel.add(helpScroller, BorderLayout.CENTER);
+ getContentPane().add(mainPanel, BorderLayout.CENTER);
+
+ pack();
+ }
+
+ public void show(Component parent) {
+ setLocationRelativeTo(parent);
+ setVisible(true);
+ }
+
+}
+
+
+class AboutWindow extends JFrame {
+ private static AboutWindow instance = null;
+
+ public static synchronized AboutWindow getInstance() {
+ if (instance == null)
+ instance = new AboutWindow();
+
+ return instance;
+ }
+
+ private AboutWindow() {
+ super("About ...");
+
+ getContentPane().setLayout(new BorderLayout());
+
+ JPanel infoPanel = new JPanel();
+ infoPanel.add(new JLabel("" + ReacticsGUI.ApplicationName + "
"
+ + "version " + ReacticsGUI.ApplicationVersion + " (" + ReacticsGUI.ApplicationReleaseDate + ")
"
+ + "Model Checker for Reaction Systems
"
+ + "ReactICS Research Team (CC BY 4.0)
"
+ + ""));
+ getContentPane().add(infoPanel, BorderLayout.CENTER);
+
+ JButton closeButton = new JButton("Close");
+ closeButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ setVisible(false);
+ }
+ });
+ JPanel ctrlPanel = new JPanel();
+ ctrlPanel.add(closeButton);
+ ctrlPanel.setAlignmentX(SwingConstants.RIGHT);
+ getContentPane().add(ctrlPanel, BorderLayout.SOUTH);
+
+ setSize(new Dimension(400, 250));
+ setResizable(false);
+ this.setAlwaysOnTop(true);
+ this.setUndecorated(true);
+ }
+
+ public void show(Component parent) {
+ setLocationRelativeTo(parent);
+ setVisible(true);
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java
new file mode 100644
index 0000000..8ace501
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java
@@ -0,0 +1,427 @@
+package pl.umk.mat.martinp.reactics;
+
+import javax.swing.*;
+import javax.swing.border.*;
+import javax.swing.table.AbstractTableModel;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.io.PrintWriter;
+import java.util.*;
+
+
+//-------------------------------------------------------------------------------------------------
+// Graphical component for editing a single process (list of reactions)
+//-------------------------------------------------------------------------------------------------
+
+class ProcessEditor extends JPanel {
+ private JTable reactionList;
+ private RSTableModel reactionsModel;
+
+ private RSProcess rsProcess;
+ private boolean modified = false;
+
+ private JCheckBox selectBox;
+ private TitledBorder outBorder;
+ private ReactionSystem rs;
+
+ private final Color borderColor = new Color(24, 104, 92);;
+ private final Color selectedBorderColor = new Color(150, 10, 10);
+ private static final int borderThickness = 4;
+
+ public ProcessEditor(RSProcess rsProc) {
+ rsProcess = rsProc;
+ init();
+ }
+
+ public RSProcess getProcess() { return rsProcess; }
+
+ public boolean isSelected() {
+ return selectBox.isSelected();
+ }
+
+ public boolean isModified() { return modified; }
+
+ public void clearModificationStatus() { modified = false; }
+
+ public String getLabel() {
+ return rsProcess.label;
+ }
+
+ private void init() {
+ // Create border for the component
+ outBorder = BorderFactory.createTitledBorder(rsProcess.label);
+ Font font = outBorder.getTitleFont();
+ Font newFont = new Font (font.getFamily(), Font.BOLD, font.getSize() + 2);
+ outBorder.setTitleFont(new Font (font.getFamily(), Font.BOLD, font.getSize() + 2));
+ outBorder.setTitleColor(borderColor);
+ outBorder.setBorder(new LineBorder(borderColor, borderThickness, true));
+ setBorder(outBorder);
+
+ // Create reactions list component
+ reactionsModel = new RSTableModel();
+ reactionList = new JTable(reactionsModel);
+
+ Font cellFont = reactionList.getFont();
+ Font headerFont = reactionList.getTableHeader().getFont();
+
+ reactionList.setFont(new Font("Monospaced", 0, cellFont.getSize() + 2));
+ reactionList.getTableHeader().setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2));
+ reactionList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+
+ setLayout(new BoxLayout(this, BoxLayout.Y_AXIS));
+
+ JPanel buttonPanel = new JPanel();
+
+ JButton addButton = new JButton("Add reaction");
+ addButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { addReaction(); }
+ });
+ buttonPanel.add(addButton);
+
+ JButton edtButton = new JButton("Edit reaction");
+ edtButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ editReaction();
+ }
+ });
+ buttonPanel.add(edtButton);
+
+ JButton rmButton = new JButton("Remove reaction");
+ rmButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ removeReactions();
+ }
+ });
+ buttonPanel.add(rmButton);
+
+ selectBox = new JCheckBox("Select");
+ selectBox.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ toggleSelection();
+ }
+ });
+ buttonPanel.add(selectBox);
+
+ add(buttonPanel);
+
+ add(new JScrollPane(reactionList));
+
+ setPreferredSize(new Dimension(-1, 200));
+
+ rs = ReactionSystem.getInstance();
+ }
+
+ private boolean showReactionEditDialog(JComponent parent, Reaction rr) {
+ final int Select = 0;
+ final int Approve = 1;
+
+ JTextField reactantsInput = new JTextField(30);
+ JTextField inhibitorsInput = new JTextField(30);
+ JTextField productsInput = new JTextField(30);
+
+ String reactantsStr = "";
+ String inhibitorsStr = "";
+ String productsStr = "";
+
+ Iterator it = rr.reactants.iterator();
+ StringBuilder dataStr = new StringBuilder();
+
+ while (it.hasNext())
+ dataStr.append(it.next()).append(" ");
+
+ reactantsStr = dataStr.toString();
+
+ it = rr.inhibitors.iterator();
+ dataStr.setLength(0);
+
+ while (it.hasNext())
+ dataStr.append(it.next()).append(" ");
+
+ inhibitorsStr = dataStr.toString();
+
+ it = rr.products.iterator();
+ dataStr.setLength(0);
+
+ while (it.hasNext())
+ dataStr.append(it.next()).append(" ");
+
+ productsStr = dataStr.toString();
+
+ reactantsInput.setToolTipText("Space separated list of reactants");
+ inhibitorsInput.setToolTipText("Space separated list of inhibitors");
+ productsInput.setToolTipText("Space separated list of products");
+
+ JPanel myPanel = new JPanel(new GridBagLayout());
+ GridBagConstraints cs = new GridBagConstraints();
+
+ cs.insets = new Insets(5, 5, 5, 5);
+ cs.anchor = GridBagConstraints.WEST;
+ cs.gridx = 0;
+ cs.gridy = 0;
+ myPanel.add(new JLabel("Reactants"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 0;
+ myPanel.add(reactantsInput, cs);
+
+ cs.gridx = 0;
+ cs.gridy = 1;
+ myPanel.add(new JLabel("Inhibitors"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 1;
+ myPanel.add(inhibitorsInput, cs);
+
+ cs.gridx = 0;
+ cs.gridy = 2;
+ myPanel.add(new JLabel("Products"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 2;
+ myPanel.add(productsInput, cs);
+
+ int opStatus = Select;
+
+ do {
+ reactantsInput.setText(reactantsStr);
+ inhibitorsInput.setText(inhibitorsStr);
+ productsInput.setText(productsStr);
+
+ int result = JOptionPane.showConfirmDialog(parent, myPanel,
+ "Reaction details", JOptionPane.OK_CANCEL_OPTION);
+
+ if (result != JOptionPane.OK_OPTION) {
+ return false;
+ }
+
+ reactantsStr = reactantsInput.getText();
+ inhibitorsStr = inhibitorsInput.getText();
+ productsStr = productsInput.getText();
+
+ HashSet reactantsSet = new HashSet(Arrays.asList(reactantsStr.trim().split("\\s+")));
+ HashSet inhibitorsSet = new HashSet(Arrays.asList(inhibitorsStr.trim().split("\\s+")));
+ HashSet productsSet = new HashSet(Arrays.asList(productsStr.trim().split("\\s+")));
+
+ // Verify that reactant and inhibitor sets have empty intersection
+ boolean intersection = false;
+
+ for (String entity : inhibitorsSet) {
+ if (reactantsSet.contains(entity)) {
+ intersection = true;
+ break;
+ }
+ }
+
+ if (intersection) {
+ JOptionPane.showMessageDialog(this, "Reactant and inhibitor sets have to be disjoint.", "Error", JOptionPane.ERROR_MESSAGE);
+ continue;
+ }
+
+ rr.reactants.clear();
+ rr.reactants.addAll(reactantsSet);
+ rr.inhibitors.clear();
+ rr.inhibitors.addAll(inhibitorsSet);
+ rr.products.clear();
+ rr.products.addAll(productsSet);
+
+ opStatus = Approve;
+ }
+ while(opStatus == Select);
+
+ return true;
+ }
+
+ public Set getReactantsSet() {
+ HashSet rset = new HashSet();
+
+ for (Reaction rr : rsProcess.reactions)
+ rset.addAll(rr.getReactantsSet());
+
+ return rset;
+ }
+
+ public void exportToXML(PrintWriter output) {
+ output.println(" ");
+
+ for (Reaction rr : rsProcess.reactions)
+ rr.exportToXML(output);
+
+ output.println(" ");
+ }
+
+ public String toRSSLString() {
+ StringBuilder rsslString = new StringBuilder(" " + rsProcess.label + " {\n");
+
+ for (Reaction rr : rsProcess.reactions) {
+ rsslString.append(rr.toRSSLString());
+ }
+
+ rsslString.append(" };\n");
+
+ return rsslString.toString();
+ }
+
+ void rename(String newLabel) {
+ rsProcess.label = newLabel;
+ outBorder.setTitle(rsProcess.label);
+
+ this.repaint();
+ }
+
+ // Add new reaction
+ public void addReaction(Reaction rr) {
+ rsProcess.reactions.add(rr);
+ reactionsModel.fireTableDataChanged();
+ }
+
+ private void addReaction() {
+ Reaction rr = new Reaction();
+ if (!showReactionEditDialog(this, rr))
+ return;
+
+ rsProcess.reactions.add(rr);
+ modified = true;
+ reactionsModel.fireTableDataChanged();
+ rs.notifyObservers();
+ }
+
+ // Edit details of an existing reaction
+ private void editReaction() {
+ int rIdx = reactionList.getSelectedRow();
+
+ if (rIdx == -1) {
+ JOptionPane.showMessageDialog(this, "Select the reaction to edit.", "Select reaction", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ Reaction rr = new Reaction(rsProcess.reactions.get(rIdx));
+ reactionList.clearSelection();
+ if (!showReactionEditDialog(this, rr)) {
+ return;
+ }
+
+ rsProcess.reactions.setElementAt(rr, rIdx);
+ modified = true;
+ reactionsModel.fireTableDataChanged();
+ rs.notifyObservers();
+ }
+
+ // Remove an existing reaction
+ private void removeReactions() {
+ int rIdx = reactionList.getSelectedRow();
+
+ if (rIdx == -1) {
+ JOptionPane.showMessageDialog(this, "Select the reaction to be removed.", "Select reaction", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ rsProcess.reactions.remove(rIdx);
+ reactionList.clearSelection();
+ reactionsModel.fireTableDataChanged();
+ modified = true;
+ this.repaint();
+ rs.notifyObservers();
+ }
+
+ private void toggleSelection() {
+ if (selectBox.isSelected()) {
+ outBorder.setTitleColor(selectedBorderColor);
+ outBorder.setBorder(new LineBorder(selectedBorderColor, borderThickness, true));
+ }
+ else {
+ outBorder.setTitleColor(borderColor);
+ outBorder.setBorder(new LineBorder(borderColor, borderThickness, true));
+ }
+
+ this.repaint();
+ }
+
+ class RSTableModel extends AbstractTableModel {
+
+ private String columnNames[] = {"Reactants", "Inhibitors", "Results"};
+ private Vector[] data;
+
+ public String getColumnName(int colIdx) {
+ return columnNames[colIdx];
+ }
+
+ public int getRowCount() {
+ return rsProcess.reactions.size();
+ }
+
+ public int getColumnCount() {
+ return columnNames.length;
+ }
+
+ public Object getValueAt(int row, int column) {
+ Reaction rr = rsProcess.reactions.get(row);
+
+ return switch (column) {
+ case 0 -> rr.reactants;
+ case 1 -> rr.inhibitors;
+ case 2 -> rr.products;
+ default -> "";
+ };
+ }
+
+ public boolean isCellEditable(int rowIndex, int columnIndex) {
+ return false;
+ }
+ }
+
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Object representing a single reaction
+//-------------------------------------------------------------------------------------------------
+
+class Reaction {
+ LinkedList reactants;
+ LinkedList inhibitors;
+ LinkedList products;
+
+ public Reaction() {
+ reactants = new LinkedList();
+ inhibitors = new LinkedList();
+ products = new LinkedList();
+ }
+
+ public Reaction(Reaction rr) {
+ reactants = new LinkedList(rr.reactants);
+ inhibitors = new LinkedList(rr.inhibitors);
+ products = new LinkedList(rr.products);
+ }
+
+ public Set getReactantsSet() {
+ Set rset = new HashSet();
+ rset.addAll(reactants);
+ rset.addAll(inhibitors);
+ rset.addAll(products);
+
+ return rset;
+ }
+
+ public String toRSSLString() {
+ return " {" + "{" + reactants.toString().replace("[", "").replace("]", "") + "}, " +
+ "{" + inhibitors.toString().replace("[", "").replace("]", "") + "} -> " +
+ "{" + products.toString().replace("[", "").replace("]", "") + "}" +
+ "};\n";
+ }
+
+ public void exportToXML(PrintWriter output) {
+ output.println(" ");
+
+ for (String str : reactants)
+ output.println(" " + str + "");
+
+ for (String str : inhibitors)
+ output.println(" " + str + "");
+
+ for (String str : products)
+ output.println(" " + str + "");
+
+ output.println(" ");
+ }
+}
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java
new file mode 100644
index 0000000..14a46e1
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java
@@ -0,0 +1,49 @@
+package pl.umk.mat.martinp.reactics;
+
+import javax.swing.*;
+import javax.swing.border.LineBorder;
+import javax.swing.border.TitledBorder;
+import java.awt.*;
+import java.util.*;
+import java.util.stream.Collectors;
+
+
+public class ReactantSetPanel extends JPanel implements RSObserver {
+ private final int borderThickness = 2;
+
+ JTextArea textArea = new JTextArea();
+
+ public ReactantSetPanel() {
+ textArea.setEditable(false);
+ textArea.setLineWrap(true);
+ textArea.setWrapStyleWord(false);
+ Font textFont = textArea.getFont();
+ textArea.setFont(new Font(textFont.getFamily(), Font.BOLD, textFont.getSize()+2));
+
+ this.setPreferredSize(new Dimension(-1, 75));
+
+ this.setLayout(new BorderLayout());
+ this.add(new JScrollPane(textArea), BorderLayout.CENTER);
+
+ TitledBorder outBorder = BorderFactory.createTitledBorder("Reactants");
+ Font borderFont = outBorder.getTitleFont();
+ outBorder.setTitleFont(new Font (borderFont.getFamily(), Font.BOLD, borderFont.getSize()+2));
+ outBorder.setBorder(new LineBorder(Color.black, borderThickness, true));
+ setBorder(outBorder);
+ }
+
+ public void updateReactants(Set reactantsSet) {
+ textArea.setText("");
+// textArea.setText(Arrays.toString(reactantsSet.toArray()));
+ textArea.setText(Arrays.stream(reactantsSet.toArray()).map(String::valueOf).collect(Collectors.joining(" ")));
+ }
+
+ public void clear() {
+ textArea.setText("");
+ }
+
+ public void onRSUpdate() {
+ ReactionSystem rs = ReactionSystem.getInstance();
+ updateReactants(rs.getReactants());
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java
new file mode 100644
index 0000000..10d126e
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java
@@ -0,0 +1,791 @@
+/** Main application window */
+
+package pl.umk.mat.martinp.reactics;
+
+import org.w3c.dom.Document;
+import org.xml.sax.SAXException;
+import javax.swing.*;
+import javax.swing.filechooser.FileNameExtensionFilter;
+import javax.xml.parsers.DocumentBuilder;
+import javax.xml.parsers.DocumentBuilderFactory;
+import javax.xml.parsers.ParserConfigurationException;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.io.*;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardOpenOption;
+import java.util.Collection;
+import java.util.TreeSet;
+
+
+public class ReacticsGUI extends JFrame {
+ public final static String ApplicationName = "ReactICS GUI";
+ public final static String ApplicationVersion = "0.1";
+ public final static String ApplicationReleaseDate = "2025";
+
+ private static final String defaultConfigFileName = "reactics.conf";
+
+ private JFrame window;
+ private JTabbedPane modulePane;
+ private ReactantSetPanel reactantSetPanel;
+ private ReactionSystemEditor reactionSystemEditor;
+ private ContextAutomatonEditor contextAutomatonEditor;
+ private TransitionSystemViewer transitionSystemViewer;
+ private TransitionSystemViewer compressedTransitionSystemViewer;
+ private FormulaEditor formulaEditor;
+
+ private FileSelector fileSelector;
+
+ private ReactionSystem reactionSystem;
+ private ReacticsRuntime reactics;
+
+
+ public ReacticsGUI() {
+ super(ApplicationName);
+
+ reactionSystem = ReactionSystem.getInstance();
+
+ try {
+ reactics = ReacticsRuntime.getInstance();
+ }
+ catch (ReacticsRuntimeException rre) {
+ JOptionPane.showMessageDialog(this,
+ rre.getMessage(),
+ "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE);
+ }
+
+ Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
+ setSize(new Dimension(screenSize.width-200, screenSize.height-200));
+ createMenuBar();
+ createContentPane();
+
+ fileSelector = FileSelector.getInstance();
+
+ try {
+ reactics.loadConfig(defaultConfigFileName);
+ }
+ catch (ConfigReadingError cre) {
+ System.err.println("[ReactICS] Error reading configuration: " + cre.getMessage());
+ JOptionPane.showMessageDialog(this,
+ "Could not read configuration\n" + cre.getMessage(),
+ "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE);
+ }
+ catch (InvalidRuntimeException ire) {
+ System.err.println("[ReactICS] ReactICS runtime cannot be executed" + ire.getMessage());
+ JOptionPane.showMessageDialog(this,
+ "Invalid ReactICS runtime patn\n" + ire.getMessage() +
+ "\nYou may proceed with editing reaction system structure," +
+ "however not model checking will be possible.",
+ "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE);
+ }
+
+ window = this;
+ }
+
+ private void createMenuBar() {
+ JMenuBar menuBar = new JMenuBar();
+
+ JMenu fileMenu = new JMenu("File");
+ menuBar.add(fileMenu);
+
+ JMenuItem xmlLoadItem = new JMenuItem("Load from XML file");
+ xmlLoadItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ loadFromXML();
+ }
+ });
+ fileMenu.add(xmlLoadItem);
+
+ JMenuItem xmlsaveItem = new JMenuItem("Save to XML file");
+ xmlsaveItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ saveAsXML();
+ }
+ });
+ fileMenu.add(xmlsaveItem);
+
+ JMenuItem rsslImportItem = new JMenuItem("Import from RSSL file");
+ rsslImportItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ importFromRSSL();
+ }
+ });
+ fileMenu.add(rsslImportItem);
+
+ JMenuItem rsslExportItem = new JMenuItem("Save to RSSL file");
+ rsslExportItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ exportToRSSLFile();
+ }
+ });
+ fileMenu.add(rsslExportItem);
+
+ JMenuItem isplExportItem = new JMenuItem("Export to ISPL file");
+ isplExportItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { exportToISPLFile(); }
+ });
+ fileMenu.add(isplExportItem);
+
+ JMenuItem exitItem = new JMenuItem("Exit");
+ exitItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ System.exit(0);
+ }
+ });
+ fileMenu.addSeparator();
+ fileMenu.add(exitItem);
+
+ JMenu helpMenu = new JMenu("Help");
+ menuBar.add(helpMenu);
+
+ JMenuItem helpItem = new JMenuItem("Help");
+ helpItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { showHelpWindow(); }
+ });
+ helpMenu.add(helpItem);
+
+ JMenuItem aboutItem = new JMenuItem("About");
+ aboutItem.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { showAboutWindow(); }
+ });
+ helpMenu.add(aboutItem);
+
+ setJMenuBar(menuBar);
+ }
+
+ private void createContentPane() {
+ modulePane = new JTabbedPane();
+ modulePane.setTabPlacement(JTabbedPane.NORTH);
+
+ //-----------------------------------------------------------------------------------------
+ // Reaction System Editor
+ //-----------------------------------------------------------------------------------------
+
+ reactionSystemEditor = new ReactionSystemEditor();
+ modulePane.addTab("Reaction System", reactionSystemEditor);
+ reactionSystem.addObserver(reactionSystemEditor);
+
+
+ //-----------------------------------------------------------------------------------------
+ // Context Automaton Editor
+ //-----------------------------------------------------------------------------------------
+
+ contextAutomatonEditor = new ContextAutomatonEditor(getSize());
+ modulePane.addTab("Context Automaton", contextAutomatonEditor);
+ reactionSystem.addObserver(contextAutomatonEditor);
+
+
+ //-----------------------------------------------------------------------------------------
+ // Transition System Viewer
+ //-----------------------------------------------------------------------------------------
+
+ JPanel transitionSystemPanel = new JPanel(new BorderLayout());
+ transitionSystemViewer = new TransitionSystemViewer(getSize(), false);
+ transitionSystemPanel.add(transitionSystemViewer, BorderLayout.CENTER);
+ reactionSystem.addObserver(transitionSystemViewer);
+
+ JPanel tsCtrlPanel = new JPanel();
+ JButton tsUpdateBtn = new JButton("Update transition system");
+ tsUpdateBtn.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { updateTransitionSystem(); }
+ });
+ tsCtrlPanel.add(tsUpdateBtn);
+
+ JCheckBox tsLockCBox = new JCheckBox("Lock relative nodes positions");
+ tsLockCBox.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ transitionSystemViewer.lockNodesPositions(tsLockCBox.isSelected());
+ }
+ });
+ tsCtrlPanel.add(tsLockCBox);
+
+ transitionSystemPanel.add(tsCtrlPanel, BorderLayout.NORTH);
+ modulePane.addTab("Transition System", transitionSystemPanel);
+
+ //-----------------------------------------------------------------------------------------
+ // Compressed Transition System Viewer
+ //-----------------------------------------------------------------------------------------
+
+ JPanel compressedTransitionSystemPanel = new JPanel(new BorderLayout());
+ compressedTransitionSystemViewer = new TransitionSystemViewer(getSize(), true);
+ compressedTransitionSystemPanel.add(compressedTransitionSystemViewer, BorderLayout.CENTER);
+ reactionSystem.addObserver(compressedTransitionSystemViewer);
+
+ JPanel ctsCtrlPanel = new JPanel();
+ JButton ctsUpdateBtn = new JButton("Update transition system");
+ ctsUpdateBtn.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { updateTransitionSystem(); }
+ });
+ ctsCtrlPanel.add(ctsUpdateBtn);
+
+ JCheckBox ctsLockCBox = new JCheckBox("Lock relative nodes positions");
+ ctsLockCBox.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ compressedTransitionSystemViewer.lockNodesPositions(ctsLockCBox.isSelected());
+ }
+ });
+ ctsCtrlPanel.add(ctsLockCBox);
+
+ compressedTransitionSystemPanel.add(ctsCtrlPanel, BorderLayout.NORTH);
+ modulePane.addTab("Compressed Transition System", compressedTransitionSystemPanel);
+
+ //-----------------------------------------------------------------------------------------
+ // Formula Editor
+ //-----------------------------------------------------------------------------------------
+
+ JPanel formulaEditorPanel = new JPanel();
+ formulaEditorPanel.setLayout(new BorderLayout());
+ formulaEditor = new FormulaEditor(reactionSystem);
+ reactionSystem.addObserver(formulaEditor);
+ formulaEditorPanel.add(formulaEditor, BorderLayout.CENTER);
+
+ JPanel formulaCtrlPanel = new JPanel();
+ JButton addButton = new JButton("Add formula");
+ addButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { formulaEditor.addFormula(window); }
+ });
+ formulaCtrlPanel.add(addButton);
+
+ JButton edtButton = new JButton("Edit formula");
+ edtButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ formulaEditor.editFormula(window);
+ }
+ });
+ formulaCtrlPanel.add(edtButton);
+
+ JButton rmButton = new JButton("Remove formulas");
+ rmButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ formulaEditor.removeFormulas();
+ }
+ });
+ formulaCtrlPanel.add(rmButton);
+
+ JButton evalButton = new JButton("Evaluate");
+ evalButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ evaluateFormulas();
+ }
+ });
+ formulaCtrlPanel.add(evalButton);
+
+ JButton resetButton = new JButton("Reset");
+ resetButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ formulaEditor.resetFormulasStatus();
+ }
+ });
+ formulaCtrlPanel.add(resetButton);
+
+ formulaEditorPanel.add(formulaCtrlPanel, BorderLayout.NORTH);
+
+ //-----------------------------------------------------------------------------------------
+ // Split the main window into two parts. The upper one contains details of the reaction
+ // system. The bottom part contains the list of formulas for model checking.
+ //-----------------------------------------------------------------------------------------
+
+ JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, modulePane, formulaEditorPanel);
+ splitPane.setResizeWeight(0.75);
+// splitPane.setOneTouchExpandable(true);
+ splitPane.setDividerSize(8);
+
+ getContentPane().setLayout(new BorderLayout());
+ getContentPane().add(splitPane, BorderLayout.CENTER);
+
+ //-----------------------------------------------------------------------------------------
+ // Update button + Reactant Set Viewer
+ //-----------------------------------------------------------------------------------------
+
+ JPanel topPanel = new JPanel();
+ topPanel.setLayout(new BorderLayout());
+ JPanel buttonPanel = new JPanel();
+ buttonPanel.setLayout(new BoxLayout(buttonPanel, BoxLayout.Y_AXIS));
+
+ JButton updateButton = new JButton("Update
Reaction System");
+ updateButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ updateReactionSystem();
+ }
+ });
+ buttonPanel.add(updateButton);
+ topPanel.add(buttonPanel, BorderLayout.WEST);
+ reactantSetPanel = new ReactantSetPanel();
+ reactionSystem.addObserver(reactantSetPanel);
+ topPanel.add(reactantSetPanel, BorderLayout.CENTER);
+ getContentPane().add(topPanel, BorderLayout.NORTH);
+ }
+
+ private boolean isModified() {
+ return reactionSystemEditor.isModified() || contextAutomatonEditor.isModified();
+ }
+
+ private void clearModificationStatus() {
+ reactionSystemEditor.clearModificationStatus();
+ contextAutomatonEditor.clearModificationStatus();
+ transitionSystemViewer.clearModificationStatus();
+ compressedTransitionSystemViewer.clearModificationStatus();
+ }
+
+ private void updateReactionSystem() {
+ System.out.println("[ReactICS] Update reaction system structure");
+
+ Path rsslFile = reactics.getRSSLFile();
+
+ try {
+ Files.writeString(rsslFile, "");
+
+ PrintWriter rsslStream = new PrintWriter(Files.newBufferedWriter(rsslFile));
+ printRSStructure(rsslStream);
+ rsslStream.close();
+ }
+ catch (IOException ie) {
+ System.err.println("[ReactICS] Could not read transition system structure: " + ie.getMessage());
+
+ JOptionPane.showMessageDialog(this,
+ "Could not read transition system structure\n" + ie.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+
+ reactionSystem.notifyObservers();
+ updateReactantSet();
+ clearModificationStatus();
+ }
+
+ private void updateReactantSet() {
+ TreeSet rset = new TreeSet();
+
+ rset.addAll(reactionSystemEditor.getReactantsSet());
+ rset.addAll(contextAutomatonEditor.getReactantsSet());
+ rset.remove("");
+ reactantSetPanel.updateReactants(rset);
+ }
+
+ private void updateTransitionSystem() {
+ if (isModified()) {
+ updateReactionSystem();
+ }
+ else if (transitionSystemViewer.isComputed()) {
+ // Skip re-computing transition system structure
+ return;
+ }
+
+ try {
+ String tsStructure = reactics.getTransitionSystemStructure();
+ transitionSystemViewer.updateTransitionSystemStructure(tsStructure);
+ compressedTransitionSystemViewer.updateTransitionSystemStructure(tsStructure);
+ }
+ catch (IOException ioe) {
+ System.out.println("[ReactICS] I/O Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this,
+ "Could not write reaction system structure to a temporary file\n" + ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ catch (ReacticsRuntimeException rre) {
+ System.out.println("[ReactICS] Runtime Error: " + rre.getMessage());
+ JOptionPane.showMessageDialog(this,
+ rre.getMessage(),
+ "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE);
+ }
+ }
+
+ private void evaluateFormulas() {
+ Collection formulas = formulaEditor.getSelectedFormulas();
+
+ if (isModified())
+ updateReactionSystem();
+
+ Path rsslFile = reactics.getRSSLFile();
+ long originalSize = -1;
+
+ try {
+ originalSize = Files.size(rsslFile);
+ }
+ catch (IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+
+ for (Formula ff : formulas) {
+ try {
+ System.out.println("[ReactICS] Evaluate formula: " + ff.label);
+
+ Files.writeString(rsslFile, ff.toRSSLString() + "\n", StandardCharsets.UTF_8, StandardOpenOption.APPEND);
+
+ ReacticsRuntime.EvalResult result = reactics.evaluateFormula(ff.label);
+ ff.status = result.result();
+ ff.mcTime = result.mcTime() + " s";
+ ff.totalTime = result.totalTime() + " s";
+ ff.memory = result.memory() + " MB";
+ formulaEditor.refreshStatus();
+ }
+ catch(IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ catch(ReacticsRuntimeException rre) {
+ System.err.println("[ReactICS] Runtime error: " + rre.getMessage());
+ JOptionPane.showMessageDialog(this,
+ rre.getMessage(),
+ "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE);
+
+ ff.status = Formula.FormulaStatus.Invalid;
+ }
+ finally {
+ try {
+ RandomAccessFile raf = new RandomAccessFile(rsslFile.toFile(), "rw");
+ raf.setLength(originalSize);
+ }
+ catch (IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ }
+ }
+ }
+
+ private void saveAsXML() {
+ File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")),
+ new FileNameExtensionFilter("Reaction System (XML)", "xml"));
+
+ if(outFile == null)
+ return;
+
+ System.out.println("[ReactICS] Save to XML file: " + outFile.getName());
+
+ try {
+ PrintWriter xmlOut = new PrintWriter(new FileWriter(outFile));
+ xmlOut.println("");
+ reactionSystemEditor.exportToXML(xmlOut);
+ contextAutomatonEditor.exportToXML(xmlOut);
+ formulaEditor.exportToXML(xmlOut);
+ xmlOut.println("");
+ xmlOut.flush();
+ xmlOut.close();
+ }
+ catch(IOException ioe) {
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ }
+
+ private void loadFromXML() {
+ FileNameExtensionFilter fileTypeFilter = new FileNameExtensionFilter("Reaction System (XML)", "xml");
+ JFileChooser fc = new JFileChooser();
+ fc.addChoosableFileFilter(fileTypeFilter);
+ fc.setAcceptAllFileFilterUsed(true);
+ fc.setCurrentDirectory(new File(System.getProperty("user.dir")));
+
+
+ if(fc.showOpenDialog(this) == JFileChooser.APPROVE_OPTION) {
+ File xmlFile = fc.getSelectedFile();
+ loadFromXMLFile(xmlFile);
+ setTitle("ReactICS GUI : " + xmlFile.getName());
+ }
+
+ modulePane.setSelectedIndex(0);
+ clearModificationStatus();
+ }
+
+
+ private void loadFromXMLFile(File xmlFile) {
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ transitionSystemViewer.clear();
+ compressedTransitionSystemViewer.clear();
+
+ try {
+ DocumentBuilderFactory dbFactory = DocumentBuilderFactory.newInstance();
+ DocumentBuilder dBuilder = dbFactory.newDocumentBuilder();
+ Document doc = dBuilder.parse(xmlFile);
+ doc.getDocumentElement().normalize();
+ reactionSystemEditor.loadFromXML(doc);
+ contextAutomatonEditor.loadFromXML(doc);
+ formulaEditor.loadFromXML(doc);
+ updateReactionSystem();
+ }
+ catch(IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+
+ JOptionPane.showMessageDialog(this, "Error reading file: " + xmlFile.getName() + "\n" + ioe.getMessage(),
+ "Input error", JOptionPane.ERROR_MESSAGE);
+
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ }
+ catch(ParserConfigurationException pce) {
+ System.err.println("[ReactICS] Parse Configuration Error: " + pce.getMessage());
+
+ JOptionPane.showMessageDialog(this, pce.getMessage(),
+ "Parse Configuration Error", JOptionPane.ERROR_MESSAGE);
+
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ }
+ catch(SAXException se) {
+ System.err.println("[ReactICS] SAXException: " + se.getMessage());
+
+ JOptionPane.showMessageDialog(this, se.getMessage(),
+ "Parse error", JOptionPane.ERROR_MESSAGE);
+
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ }
+ catch(FileStructureError err) {
+ System.err.println("[ReactICS]: File Structure Error: " + err.getMessage());
+
+ JOptionPane.showMessageDialog(this, err.getMessage(),
+ "XML file structure error", JOptionPane.ERROR_MESSAGE);
+
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ }
+ catch(Exception e) {
+ System.out.println("[ReactICS] Error: " + e.getMessage());
+
+ JOptionPane.showMessageDialog(this, "Unexpected error reading file: " + xmlFile.getName() +
+ " " + e.getMessage(),
+ "Input error", JOptionPane.ERROR_MESSAGE);
+
+ reactionSystemEditor.clear();
+ contextAutomatonEditor.clear();
+ reactantSetPanel.clear();
+ }
+ }
+
+
+ private void importFromRSSL() {
+ FileNameExtensionFilter fileTypeFilter = new FileNameExtensionFilter("Reaction System Specification Language (rs)", "rs");
+ JFileChooser fc = new JFileChooser();
+ fc.addChoosableFileFilter(fileTypeFilter);
+ fc.setAcceptAllFileFilterUsed(true);
+ fc.setCurrentDirectory(new File(System.getProperty("user.dir")));
+
+
+ if(fc.showOpenDialog(this) == JFileChooser.APPROVE_OPTION) {
+ File rsslFile = fc.getSelectedFile();
+
+ try {
+ File xmlFile = reactics.convertToXMLFile(rsslFile);
+ loadFromXMLFile(xmlFile);
+ } catch (IOException e) {
+ System.err.println("IOException: " + e.getMessage());
+ e.printStackTrace();
+ } catch (ReacticsRuntimeException e) {
+ System.err.println("ReacticsRuntimeException: " + e.getMessage());
+ e.printStackTrace();
+ }
+
+ setTitle("ReactICS GUI : " + rsslFile.getName());
+ contextAutomatonEditor.recalculateCoordinates();
+ }
+
+ modulePane.setSelectedIndex(0);
+ clearModificationStatus();
+ }
+
+
+ private void exportToRSSLFile() {
+ File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")),
+ new FileNameExtensionFilter("Reaction System Specification Language (RSSL)", "rs"));
+
+ if(outFile == null)
+ return;
+
+ System.out.println("[ReactICS] Export to RSSL file: " + outFile.getName());
+
+ try {
+ PrintWriter rsslOut = new PrintWriter(new FileWriter(outFile));
+ printRSStructure(rsslOut);
+ rsslOut.close();
+ }
+ catch(IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ }
+
+
+ private void exportToISPLFile() {
+ updateReactionSystem();
+
+ if (!reactionSystem.isplTranslationAllowed()) {
+ JOptionPane.showMessageDialog(this,
+ "Context automaton contains guards for some transitions.\n" +
+ "Current version of ReactICS does not support translation to ISPL format in this case.\n",
+ "Translation is not possible", JOptionPane.INFORMATION_MESSAGE);
+ return;
+ }
+
+ File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")),
+ new FileNameExtensionFilter("Interpreted System Programming Language (ISPL)", "ispl"));
+
+ if (outFile == null)
+ return;
+
+ System.out.println("[ReactICS] Export to ISPL file: " + outFile.getAbsolutePath());
+
+ try {
+ if (!outFile.exists() && !outFile.createNewFile()) {
+ System.err.println("[ReactICS] Error: The file "+ outFile.getName() + " could not be created.");
+ JOptionPane.showMessageDialog(this,
+ "The file " + outFile.getName() + " could not be created.",
+ "Error", JOptionPane.ERROR_MESSAGE);
+ return;
+ }
+
+ if (!outFile.canWrite()){
+ System.err.println("[ReactICS] Error: Cannot write to the file " + outFile.getName());
+ JOptionPane.showMessageDialog(this,
+ "Cannot write to the file " + outFile.getName(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ return;
+ }
+
+ reactics.exportToISPLFile(outFile);
+ }
+ catch(IOException ioe) {
+ System.err.println("[ReactICS] Error: " + ioe.getMessage());
+ JOptionPane.showMessageDialog(this, ioe.getMessage(),
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ catch(ReacticsRuntimeException rre) {
+ System.err.println("[ReactICS] Runtime error: " + rre.getMessage());
+ JOptionPane.showMessageDialog(this,
+ rre.getMessage(),
+ "ReactICS Runtime Error", JOptionPane.ERROR_MESSAGE);
+ }
+ }
+
+ private void printRSStructure(PrintWriter outStream) {
+ outStream.println("options { use-context-automaton; make-progressive; };\n");
+ outStream.println(reactionSystemEditor.toRSSLString());
+ outStream.println(contextAutomatonEditor.toRSSLString());
+ }
+
+ private void showAboutWindow() {
+ AboutWindow awin = AboutWindow.getInstance();
+ awin.show(this);
+ }
+
+ private void showHelpWindow() {
+ HelpWindow hwin = HelpWindow.getInstance();
+ hwin.show(this);
+ }
+
+ public static void main(String args[]) {
+ ReacticsGUI wnd = new ReacticsGUI();
+ wnd.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
+ wnd.setLocationRelativeTo(null);
+ wnd.setVisible(true);
+ }
+
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Class responsible for selecting a file to load / save the reaction system structure
+//-------------------------------------------------------------------------------------------------
+
+class FileSelector {
+ private enum Status {SELECT, APPROVE, CANCEL}
+
+ private static FileSelector instance = null;
+
+ public static synchronized FileSelector getInstance() {
+ if (instance == null)
+ instance = new FileSelector();
+
+ return instance;
+ }
+
+ private FileSelector() { }
+
+ public File selecInputFile(Component parent, File rootDir, FileNameExtensionFilter filter) {
+ Status opStatus = Status.SELECT;
+ JFileChooser fc = new JFileChooser();
+ fc.addChoosableFileFilter(filter);
+ fc.setAcceptAllFileFilterUsed(true);
+ fc.setCurrentDirectory(rootDir);
+ File outFile = null;
+
+ do {
+ if (fc.showOpenDialog(parent) != JFileChooser.APPROVE_OPTION) {
+ opStatus = Status.CANCEL;
+ break;
+ }
+
+ outFile = fc.getSelectedFile();
+ opStatus = Status.APPROVE;
+
+ if(outFile.exists()) {
+ if (JOptionPane.showConfirmDialog(parent,
+ "The file " + outFile.getName() + " already exists.\n" +
+ "Do you wish to overwrite it?", "Warning",
+ JOptionPane.YES_NO_OPTION, JOptionPane.WARNING_MESSAGE) == JOptionPane.NO_OPTION) {
+ opStatus = Status.SELECT;
+ }
+ }
+ } while(opStatus == Status.SELECT);
+
+ if(opStatus != Status.APPROVE)
+ outFile = null;
+
+ return outFile;
+ }
+
+ public File selectOutputFile(Component parent, File rootDir, FileNameExtensionFilter filter) {
+ Status opStatus = Status.SELECT;
+ JFileChooser fc = new JFileChooser();
+ fc.addChoosableFileFilter(filter);
+ fc.setAcceptAllFileFilterUsed(true);
+ fc.setCurrentDirectory(rootDir);
+ File outFile = null;
+
+ do {
+ if (fc.showSaveDialog(parent) != JFileChooser.APPROVE_OPTION) {
+ opStatus = Status.CANCEL;
+ break;
+ }
+
+ outFile = fc.getSelectedFile();
+ opStatus = Status.APPROVE;
+
+ if(outFile.exists()) {
+ if (JOptionPane.showConfirmDialog(parent,
+ "The file " + outFile.getName() + " already exists.\n" +
+ "Do you wish to overwrite it?", "Warning",
+ JOptionPane.YES_NO_OPTION, JOptionPane.WARNING_MESSAGE) == JOptionPane.NO_OPTION) {
+ opStatus = Status.SELECT;
+ }
+ }
+ } while(opStatus == Status.SELECT);
+
+ if(opStatus != Status.APPROVE)
+ outFile = null;
+
+ return outFile;
+ }
+}
+
+
+/**
+ * General exception class for any error related to input XML file
+ */
+class FileStructureError extends Exception {
+ public FileStructureError(String message) {
+ super(message);
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java
new file mode 100644
index 0000000..d8c73ea
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java
@@ -0,0 +1,198 @@
+package pl.umk.mat.martinp.reactics;
+
+import java.io.*;
+import java.nio.file.Files;
+import java.nio.file.Path;
+
+
+public class ReacticsRuntime {
+ private static ReacticsRuntime instance = null;
+
+ private String rctPath = "./";
+ private String rctRuntime = "reactics";
+ private Path rsslFile;
+
+ public static synchronized ReacticsRuntime getInstance() throws ReacticsRuntimeException {
+ if (instance == null)
+ instance = new ReacticsRuntime();
+
+ return instance;
+ }
+
+ private ReacticsRuntime() throws ReacticsRuntimeException {
+ try {
+ rsslFile = Files.createTempFile("reaction_system_", ".rs");
+ rsslFile.toFile().deleteOnExit();
+ System.out.println("[ReactICS] Created temporary file: " + rsslFile.toAbsolutePath());
+ }
+ catch (IOException e) {
+ System.err.println("[ReactICS] Problem creating temporary file: + e.getMessage()");
+ throw new ReacticsRuntimeException("Problem creating temporary file:\n" + e.getMessage());
+ }
+ }
+
+ public Path getRSSLFile() {
+ return rsslFile;
+ }
+
+ public void loadConfig(String configFileName) throws ConfigReadingError, InvalidRuntimeException {
+ System.out.println("[ReactICS] Loading configuration from: " + configFileName);
+
+ try {
+ BufferedReader inputStream = new BufferedReader(new FileReader(configFileName));
+ String line;
+
+ while ((line = inputStream.readLine()) != null) {
+ if (line.startsWith("runtime")) {
+ line = line.replaceAll("\\s", "");
+ rctRuntime = line.substring(line.indexOf(":") + 1);
+ }
+ else if (line.startsWith("path")) {
+ line = line.replaceAll("\\s", "");
+ rctPath = line.substring(line.indexOf(":") + 1);
+ }
+ }
+ }
+ catch (IOException e) {
+ throw new ConfigReadingError(e.getMessage());
+ }
+
+ File rctRntFile = new File(rctPath + rctRuntime);
+
+ if (! (rctRntFile.exists() && rctRntFile.canExecute()) ) {
+ throw new InvalidRuntimeException(rctPath + rctRuntime + " cannot be executed");
+ }
+
+ System.out.println("[ReactICS] Using runtime: " + rctPath + rctRuntime);
+ }
+
+ public EvalResult evaluateFormula(String fLabel) throws IOException, ReacticsRuntimeException {
+ // Drop "-B" option if verification time should not be measured
+ Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -B -c " + fLabel + " " + rsslFile.toAbsolutePath(),
+ null, new File(rctPath));
+
+ BufferedReader formResultStream = new BufferedReader(new InputStreamReader(proc.getInputStream()));
+ String line;
+ Formula.FormulaStatus result = Formula.FormulaStatus.None;
+ String mcTime = "";
+ String totalTime = "";
+ String memory = "";
+
+ while ((line = formResultStream.readLine()) != null) {
+ if (line.contains("holds")) {
+ result = Formula.FormulaStatus.True;
+ }
+ else if (line.contains("not hold")) {
+ result = Formula.FormulaStatus.False;
+ }
+ else if (line.startsWith("STAT")) {
+ String[] tokens = line.split(";");
+ mcTime = tokens[2];
+ totalTime = tokens[5];
+ memory = tokens[4];
+ }
+
+ //TODO: Handle incorrect formulas
+ }
+
+ StringBuilder errMsg = new StringBuilder();
+ BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
+ while ((line = procErrStr.readLine()) != null) {
+ errMsg.append(line).append("\n");
+ }
+
+ if (!errMsg.isEmpty())
+ throw new ReacticsRuntimeException(errMsg.toString());
+
+ return new EvalResult(result, mcTime, totalTime, memory);
+ }
+
+ /** Complete Transition System. Context automaton state included. */
+ public String getTransitionSystemStructure() throws IOException, ReacticsRuntimeException {
+ Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -t -X " + rsslFile.toAbsolutePath(),
+ null, new File(rctPath));
+
+ String line;
+ StringBuilder tsString = new StringBuilder();
+ BufferedReader procOutStr = new BufferedReader(new InputStreamReader(proc.getInputStream()));
+ while ((line = procOutStr.readLine()) != null) {
+ tsString.append(line).append("\n");
+ }
+
+ StringBuilder errMsg = new StringBuilder();
+ BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
+ while ((line = procErrStr.readLine()) != null) {
+ errMsg.append(line).append("\n");
+ }
+
+ if (!errMsg.isEmpty())
+ throw new ReacticsRuntimeException(errMsg.toString());
+
+ return tsString.toString();
+ }
+
+ public void exportToISPLFile(File outFile) throws IOException, ReacticsRuntimeException {
+ Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -e " + rsslFile.toAbsolutePath() + " > " + outFile.getAbsolutePath(),
+ null, new File(rctPath));
+
+ String line;
+ BufferedReader procOutStr = new BufferedReader(new InputStreamReader(proc.getInputStream()));
+ PrintWriter isplOutStr = new PrintWriter(new FileWriter(outFile));
+ while ((line = procOutStr.readLine()) != null) {
+ isplOutStr.println(line);
+ }
+ isplOutStr.close();
+
+ StringBuilder errMsg = new StringBuilder();
+ BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
+ while ((line = procErrStr.readLine()) != null) {
+ errMsg.append(line).append("\n");
+ }
+
+ if (!errMsg.isEmpty())
+ throw new ReacticsRuntimeException(errMsg.toString());
+ }
+
+
+ public File convertToXMLFile(File rsslInputFile) throws IOException, ReacticsRuntimeException {
+ File xmlFile = Files.createTempFile("_" + rsslInputFile.getName(), ".xml").toFile();
+ xmlFile.deleteOnExit();
+
+ ProcessBuilder procBuilder = new ProcessBuilder(rctPath + rctRuntime, "-y", rsslInputFile.getAbsolutePath());
+ procBuilder.redirectOutput(new File(xmlFile.getAbsolutePath()));
+ Process proc = procBuilder.start();
+
+ String line;
+ StringBuilder errMsg = new StringBuilder();
+ BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream()));
+ while ((line = procErrStr.readLine()) != null) {
+ errMsg.append(line).append("\n");
+ }
+
+ if (!errMsg.isEmpty())
+ throw new ReacticsRuntimeException(errMsg.toString());
+
+ return xmlFile;
+ }
+
+
+ record EvalResult(Formula.FormulaStatus result, String mcTime, String totalTime, String memory) {}
+}
+
+class ConfigReadingError extends Exception {
+ public ConfigReadingError(String message) {
+ super(message);
+ }
+}
+
+class InvalidRuntimeException extends Exception {
+ public InvalidRuntimeException(String description) {
+ super(description);
+ }
+}
+
+class ReacticsRuntimeException extends Exception {
+ public ReacticsRuntimeException(String description) {
+ super(description);
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java
new file mode 100644
index 0000000..51a86c9
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java
@@ -0,0 +1,409 @@
+/** A component for editing the reaction system details */
+
+package pl.umk.mat.martinp.reactics;
+
+import org.w3c.dom.Document;
+import org.w3c.dom.Node;
+import org.w3c.dom.NodeList;
+
+import javax.swing.*;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.io.PrintWriter;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Set;
+import java.util.Vector;
+
+
+//-------------------------------------------------------------------------------------------------
+/** A graphical component allowing edition and display of a distributed reaction system.
+ * A distributed reaction system contains a number of processes.
+ * Each process contains a list of reactions.
+ */
+public class ReactionSystemEditor extends JPanel implements RSObserver {
+ ReactionSystem rs;
+ private Vector procEditors = new Vector();
+ private JPanel processPanel = new JPanel();
+
+
+ public ReactionSystemEditor() {
+ rs = ReactionSystem.getInstance();
+
+ processPanel.setLayout(new BoxLayout(processPanel, BoxLayout.Y_AXIS));
+
+ final Dimension buttonSize = new Dimension(150, 25);
+
+ JButton addButton = new JButton("New process");
+ addButton.setMaximumSize(buttonSize);
+ addButton.setPreferredSize(buttonSize);
+ addButton.setMaximumSize(buttonSize);
+ addButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ createProcess();
+ }
+ });
+
+ JButton rmButton = new JButton("Remove");
+ rmButton.setMaximumSize(buttonSize);
+ rmButton.setPreferredSize(buttonSize);
+ rmButton.setMaximumSize(buttonSize);
+ rmButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ removeProcesses();
+ }
+ });
+
+ JButton copyButton = new JButton("Copy");
+ copyButton.setMaximumSize(buttonSize);
+ copyButton.setPreferredSize(buttonSize);
+ copyButton.setMaximumSize(buttonSize);
+ copyButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ copyProcesses();
+ }
+ });
+
+ JButton renameButton = new JButton("Rename");
+ renameButton.setMaximumSize(buttonSize);
+ renameButton.setPreferredSize(buttonSize);
+ renameButton.setMaximumSize(buttonSize);
+ renameButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ renameProcess();
+ }
+ });
+
+ JButton upButton = new JButton("Move up");
+ upButton.setMaximumSize(buttonSize);
+ upButton.setPreferredSize(buttonSize);
+ upButton.setMaximumSize(buttonSize);
+ upButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ moveSelectedUp();
+ }
+ });
+
+ JButton downButton = new JButton("Move down");
+ downButton.setMaximumSize(buttonSize);
+ downButton.setPreferredSize(buttonSize);
+ downButton.setMaximumSize(buttonSize);
+ downButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) {
+ moveSelectedDown();
+ }
+ });
+
+ JPanel buttonPanel = new JPanel();
+ buttonPanel.setLayout(new BoxLayout(buttonPanel, BoxLayout.Y_AXIS));
+
+ buttonPanel.add(addButton);
+ buttonPanel.add(rmButton);
+ buttonPanel.add(copyButton);
+ buttonPanel.add(renameButton);
+ buttonPanel.add(upButton);
+ buttonPanel.add(downButton);
+
+ this.setLayout(new BorderLayout());
+ this.add(new JScrollPane(processPanel), BorderLayout.CENTER);
+ this.add(buttonPanel, BorderLayout.WEST);
+
+ createProcess();
+ }
+
+ public boolean isModified() {
+ boolean procModified = false;
+
+ for (ProcessEditor pe : procEditors)
+ procModified |= pe.isModified();
+
+ return rs.modified | procModified;
+ }
+
+ public void clearModificationStatus() {
+ for (ProcessEditor pe : procEditors)
+ pe.clearModificationStatus();
+
+ rs.modified = false;
+ }
+
+ public Set getReactantsSet() {
+ HashSet rset = new HashSet();
+
+ for (ProcessEditor pe : procEditors)
+ rset.addAll(pe.getReactantsSet());
+
+ return rset;
+ }
+
+ public void exportToXML(PrintWriter output) {
+ output.println(" ");
+
+ for (ProcessEditor process : procEditors)
+ process.exportToXML(output);
+
+ output.println(" ");
+ }
+
+ public void loadFromXML(Document input) throws ReactionSystemStructureError {
+ NodeList rsSections = input.getElementsByTagName("reaction-system");
+
+ if (rsSections.getLength() == 0 || rsSections.getLength() > 1) {
+ throw new ReactionSystemStructureError("An XML file should contain a single reaction system description.");
+ }
+
+ NodeList processList = rsSections.item(0).getChildNodes();
+
+ for (int idx=0; idx toRemove = new Vector();
+ for (ProcessEditor edt : procEditors) {
+ if (edt.isSelected()) {
+ toRemove.add(edt);
+ }
+ }
+
+ if (toRemove.size() == procEditors.size()) {
+ JOptionPane.showMessageDialog(this, "There should be at least a single process in the system.",
+ "Warning", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ for (ProcessEditor edt : toRemove) {
+ if (rs.removeProcess(edt.getProcess())) {
+ processPanel.remove(edt);
+ procEditors.remove(edt);
+ }
+ else {
+ JOptionPane.showMessageDialog(this, "Process " + edt.getLabel() +
+ " appears in a formula or a context automaton guard.\n" +
+ "Update them before removing the process.",
+ "Warning", JOptionPane.WARNING_MESSAGE);
+ }
+ }
+
+ rs.modified = true;
+ revalidate();
+ }
+
+ private void copyProcesses() {
+ Vector toBeCopied = new Vector();
+
+ for (ProcessEditor edt : procEditors) {
+ if (edt.isSelected()) {
+ toBeCopied.add(edt);
+ }
+ }
+
+ for (ProcessEditor edt : toBeCopied) {
+ ProcessEditor newEdt = new ProcessEditor(rs.copyProcess(edt.getProcess()));
+ processPanel.add(newEdt);
+ procEditors.add(newEdt);
+ }
+
+ rs.modified = true;
+ revalidate();
+ }
+
+ private void renameProcess() {
+ ProcessEditor toRename = null;
+ boolean fail = false;
+
+ for (ProcessEditor edt : procEditors) {
+ if (edt.isSelected()) {
+ if (toRename == null) {
+ toRename = edt;
+ }
+ else {
+ fail = true;
+ break;
+ }
+ }
+ }
+
+ if (fail || toRename == null) {
+ JOptionPane.showMessageDialog(this, "Select a single process to rename.", "Select process", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ String idRegex = "[a-zA-Z][a-zA-Z_0-9:-]*";
+ boolean idOk = false;
+
+ do {
+ String newLabel = JOptionPane.showInputDialog(this, "Process name", toRename.getProcess().label);
+ if (newLabel == null)
+ return;
+
+ newLabel = newLabel.trim();
+
+ if (!newLabel.matches(idRegex)) {
+ JOptionPane.showMessageDialog(this,
+ "Process name should start with a letter and may contain only:
" +
+ "letters, numbers, colons (:), underscores (_) and hyphens (-)",
+ "Error", JOptionPane.ERROR_MESSAGE);
+ }
+ else {
+ idOk = true;
+ rs.renameProcess(toRename.getProcess(), newLabel);
+ toRename.rename(newLabel);
+ rs.notifyObservers();
+ }
+ }
+ while (!idOk);
+
+ }
+
+ private void moveSelectedUp() {
+ Vector toBeMovedIds = new Vector();
+ for (int i = 0; i< procEditors.size(); ++i) {
+ if (procEditors.elementAt(i).isSelected())
+ toBeMovedIds.add(i);
+ }
+
+ for (int pos : toBeMovedIds) {
+ if (pos == 0 || procEditors.elementAt(pos-1).isSelected())
+ continue;
+
+ Collections.swap(procEditors, pos, pos-1);
+ }
+
+ processPanel.removeAll();
+
+ for (ProcessEditor edt : procEditors) {
+ processPanel.add(edt);
+ }
+
+ rs.modified = true;
+ revalidate();
+ }
+
+ private void moveSelectedDown() {
+ Vector toBeMovedIds = new Vector();
+
+ for (int i = procEditors.size()-1; i>=0; --i) {
+ if (procEditors.elementAt(i).isSelected())
+ toBeMovedIds.add(i);
+ }
+
+ for (int pos : toBeMovedIds) {
+ if (pos == procEditors.size()-1 || procEditors.elementAt(pos+1).isSelected())
+ continue;
+
+ Collections.swap(procEditors, pos, pos+1);
+ }
+
+ processPanel.removeAll();
+
+ for (ProcessEditor edt : procEditors) {
+ processPanel.add(edt);
+ }
+
+ rs.modified = true;
+ revalidate();
+ }
+
+ public void onRSUpdate() {
+ repaint();
+ }
+
+}
+
+
+class ReactionSystemStructureError extends FileStructureError {
+ public ReactionSystemStructureError(String message) {
+ super(message);
+ }
+}
\ No newline at end of file
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java
new file mode 100644
index 0000000..b7083af
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java
@@ -0,0 +1,208 @@
+package pl.umk.mat.martinp.reactics;
+
+import javax.swing.*;
+import javax.swing.table.AbstractTableModel;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.util.*;
+
+
+class TransitionEditor extends JDialog {
+ private JTable transitionsList;
+ private TransitionTableModel transitionsModel;
+ private Vector transitions;
+
+ public TransitionEditor() {
+ super();
+
+ // Create reactions list component
+ transitionsModel = new TransitionTableModel();
+ transitionsList = new JTable(transitionsModel);
+
+ Font cellFont = transitionsList.getFont();
+ Font headerFont = transitionsList.getTableHeader().getFont();
+
+ transitionsList.setFont(new Font("Monospaced", 0, cellFont.getSize() + 2));
+ transitionsList.getTableHeader().setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2));
+ transitionsList.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
+
+ getContentPane().setLayout(new BorderLayout());
+
+ JButton addButton = new JButton("Add transition");
+ addButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { addTransition(); }
+ });
+
+ JButton edtButton = new JButton("Edit transition");
+ edtButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { editTransition(); }
+ });
+
+ JButton rmButton = new JButton("Remove transition");
+ rmButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { removeTransitions(); }
+ });
+
+ JButton closeButton = new JButton("Close");
+ closeButton.addActionListener(new ActionListener() {
+ public void actionPerformed(ActionEvent actionEvent) { setVisible(false); }
+ });
+
+ JPanel buttonPanel = new JPanel();
+ buttonPanel.add(addButton);
+ buttonPanel.add(edtButton);
+ buttonPanel.add(rmButton);
+ buttonPanel.add(closeButton);
+
+ getContentPane().add(buttonPanel, BorderLayout.NORTH);
+ getContentPane().add(new JScrollPane(transitionsList), BorderLayout.CENTER);
+
+ setPreferredSize(new Dimension(-1, 200));
+ setSize(new Dimension(600, 200));
+ setTitle("Transitions");
+ }
+
+ public void showTransitionEditDialog(Component parent, Collection trans, String from, String to) {
+ setTitle("Transitions for (" + from + " -> " + to + ")");
+ transitions = (Vector) trans;
+ transitionsModel.fireTableDataChanged();
+ setLocationRelativeTo(parent);
+ setVisible(true);
+ }
+
+ private void addTransition() {
+ Transition tr = new Transition("", "");
+
+ if (!showTransitionEditDialog(tr))
+ return;
+
+ transitions.add(tr);
+ transitionsModel.fireTableDataChanged();
+ }
+
+ private void editTransition() {
+ int[] selected = transitionsList.getSelectedRows();
+
+ if (selected.length != 1) {
+ JOptionPane.showMessageDialog(this, "Select a single transition to edit.", "Select transition", JOptionPane.WARNING_MESSAGE);
+ return;
+ }
+
+ Transition tr = transitions.get(selected[0]);
+ transitionsList.clearSelection();
+ if (!showTransitionEditDialog(tr)) {
+ return;
+ }
+
+ transitions.setElementAt(tr, selected[0]);
+ transitionsModel.fireTableDataChanged();
+ }
+
+ private void removeTransitions() {
+ int[] selected = transitionsList.getSelectedRows();
+
+ for (int trIdx : selected) {
+ transitions.remove(trIdx);
+ transitionsList.clearSelection();
+ }
+
+ transitionsModel.fireTableDataChanged();
+ }
+
+ private boolean showTransitionEditDialog(Transition tr) {
+ final int Select = 0;
+ final int Approve = 1;
+
+ JTextField contextInput = new JTextField(30);
+ JTextField guardInput = new JTextField(30);
+
+ String contextStr = tr.context;
+ String guardStr = tr.guard;
+
+ contextInput.setToolTipText("Additional entities for processes");
+ guardInput.setToolTipText("Initial conditions for the transition in rsCTL format.");
+
+ JPanel myPanel = new JPanel(new GridBagLayout());
+ GridBagConstraints cs = new GridBagConstraints();
+
+ cs.insets = new Insets(5, 5, 5, 5);
+ cs.anchor = GridBagConstraints.WEST;
+ cs.gridx = 0;
+ cs.gridy = 0;
+ myPanel.add(new JLabel("Context"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 0;
+ myPanel.add(contextInput, cs);
+
+ cs.gridx = 0;
+ cs.gridy = 1;
+ myPanel.add(new JLabel("Guards"), cs);
+
+ cs.gridx = 1;
+ cs.gridy = 1;
+ myPanel.add(guardInput, cs);
+
+ int opStatus = Select;
+
+ do {
+ contextInput.setText(contextStr);
+ guardInput.setText(guardStr);
+
+ int result = JOptionPane.showConfirmDialog(null, myPanel,
+ "Reaction details", JOptionPane.OK_CANCEL_OPTION);
+
+ if (result != JOptionPane.OK_OPTION) {
+ return false;
+ }
+
+ contextStr = contextInput.getText();
+ guardStr = guardInput.getText();
+
+ //TODO: Validate the data entered to the text fields
+ tr.context = contextStr;
+ tr.guard = guardStr;
+
+ opStatus = Approve;
+ }
+ while(opStatus == Select);
+
+ return true;
+ }
+
+
+ class TransitionTableModel extends AbstractTableModel {
+
+ private final String[] columnNames = {"Context", "Guard"};
+
+ public String getColumnName(int colIdx) {
+ return columnNames[colIdx];
+ }
+
+ public int getRowCount() {
+ return transitions.size();
+ }
+
+ public int getColumnCount() {
+ return columnNames.length;
+ }
+
+
+ public Object getValueAt(int row, int column) {
+ Transition tr = transitions.get(row);
+
+ return switch (column) {
+ case 0 -> tr.context;
+ case 1 -> tr.guard;
+ default -> "";
+ };
+ }
+
+ public boolean isCellEditable(int rowIndex, int columnIndex) {
+ return false;
+ }
+ }
+
+}
+
diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java
new file mode 100644
index 0000000..82c8949
--- /dev/null
+++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java
@@ -0,0 +1,367 @@
+package pl.umk.mat.martinp.reactics;
+
+import edu.uci.ics.jung.algorithms.layout.*;
+import edu.uci.ics.jung.algorithms.layout.util.Relaxer;
+import edu.uci.ics.jung.graph.DirectedSparseGraph;
+import edu.uci.ics.jung.visualization.VisualizationViewer;
+import edu.uci.ics.jung.visualization.control.DefaultModalGraphMouse;
+import edu.uci.ics.jung.visualization.control.ModalGraphMouse;
+import edu.uci.ics.jung.visualization.decorators.ToStringLabeller;
+import edu.uci.ics.jung.visualization.renderers.Renderer;
+import org.apache.commons.collections15.Transformer;
+
+import javax.swing.JPanel;
+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 implements RSObserver {
+
+ //---------------------------------------------------------------
+ // Visual configuration settings
+ //---------------------------------------------------------------
+
+ private static final Color pickedNodeColor = Color.yellow;
+ private static final Color edgeColor = Color.black;
+ private static final Font nodeLabelFont = new Font("Helvetica", Font.BOLD, 20);
+ private static final Font toolTipFont = new Font("Helvetica", Font.PLAIN, 14);
+ private static final Stroke basicEdgeArrow = new BasicStroke(3.0f);
+
+ private static Dimension initialEditorSize;
+
+ private VisualizationViewer graphViewer;
+ private Layout graphLayout;
+ DefaultModalGraphMouse graphMouse;
+
+ //---------------------------------------------------------------
+ // Transition system graph
+ //---------------------------------------------------------------
+
+ private DirectedSparseGraph tsGraph;
+ private boolean isCompressed;
+
+ // Is transition system already computed?
+ // Used to avoid unnecessary computation of the same graph.
+ private boolean computed = false;
+
+ // compressed == true => context automaton state is not taken into account.
+ public TransitionSystemViewer(Dimension size, boolean compressed) {
+ this.setLayout(new BorderLayout());
+ tsGraph = new DirectedSparseGraph();
+ this.isCompressed = compressed;
+ initialEditorSize = size;
+
+ createGraphViever();
+ lockNodesPositions(false);
+ }
+
+ // Is transition system graph already computed?
+ boolean isComputed() { return computed; }
+
+ void clearModificationStatus() { computed = false; }
+
+ private void createGraphViever() {
+ graphLayout = new FRLayout(tsGraph);
+
+ graphViewer = new VisualizationViewer(graphLayout, initialEditorSize) {
+ public JToolTip createToolTip() {
+ JToolTip tooltip = super.createToolTip();
+ tooltip.setFont(toolTipFont);
+ return tooltip;
+ }
+ };
+
+ // Nodes labels
+ graphViewer.getRenderContext().setVertexLabelTransformer(
+ new ToStringLabeller());
+ graphViewer.getRenderer().getVertexLabelRenderer()
+ .setPosition(Renderer.VertexLabel.Position.CNTR);
+ graphViewer.getRenderContext().setVertexFontTransformer(
+ new Transformer() {
+ public Font transform(TSState st) {
+ return nodeLabelFont;
+ }
+ });
+
+ // Nodes colour, background, etc.
+ graphViewer.getRenderContext().setVertexIconTransformer(new Transformer() {
+ public Icon transform(final TSState v) {
+ Color nodeColor = null;
+
+ if(graphViewer.getPickedVertexState().isPicked(v))
+ nodeColor = pickedNodeColor;
+ else
+ nodeColor = v.getFillColor();
+
+ return (v.isInitial() ? new SquareIcon(nodeColor, v.getWidth()) : new CircleIcon(nodeColor, v.getWidth()));
+
+ }});
+
+ graphViewer.getRenderContext().setEdgeShapeTransformer(new ConditionalEdgeShape<>(1.5f));
+
+ // Edges
+ graphViewer.getRenderContext().setEdgeArrowStrokeTransformer(new Transformer() {
+ public Stroke transform(TSTransition tr) {
+ return basicEdgeArrow;
+ }
+ });
+
+ // For interactive graph editing
+ graphMouse = new DefaultModalGraphMouse();
+ graphViewer.setGraphMouse(graphMouse);
+ graphMouse.setMode(ModalGraphMouse.Mode.PICKING);
+
+ graphViewer.setVertexToolTipTransformer(new Transformer() {
+ public String transform(TSState st) {
+ return st.getTooltipText();
+ }
+ });
+
+ graphViewer.setBackground(Color.white);
+ graphViewer.setBorder(new EtchedBorder(EtchedBorder.LOWERED));
+
+ add(graphViewer, BorderLayout.CENTER);
+ }
+
+
+ public void updateTransitionSystemStructure(String tsString) {
+ // Clear graph
+ clear();
+
+ // Load graph structure
+ int nextId = 1;
+
+ HashMap nodes = new HashMap<>();
+ TSState src = null;
+
+ for (String line : tsString.split("\\R")) {
+ char type = line.charAt(0);
+ line = line.substring(2).strip();
+ int end = line.lastIndexOf('}');
+ String automatonState = line.substring(end + 1, line.length() - 1).strip();
+ String stateStr = line.substring(line.indexOf('{'), end + 1);
+ TSState state = nodes.get( isCompressed ? stateStr : line);
+
+ if (state == null) {
+ state = new TSState(nextId++, stateStr, isCompressed ? null : automatonState);
+ nodes.put(isCompressed ? stateStr : line, state);
+ tsGraph.addVertex(state);
+ }
+
+ if (type == 'G') {
+ src = state;
+ }
+ else if (type == 's') {
+ tsGraph.addEdge(new TSTransition(), src, state);
+ }
+ }
+
+ // Find the initial state
+ for (TSState state : tsGraph.getVertices()) {
+ if (tsGraph.getInEdges(state).size() == 0) {
+ state.setAsInitial();
+ break;
+ }
+ }
+
+ relax();
+ graphViewer.repaint();
+ computed = true;
+ }
+
+
+ public void lockNodesPositions(boolean lock) {
+ if (lock)
+ graphMouse.setMode(ModalGraphMouse.Mode.TRANSFORMING);
+ else
+ graphMouse.setMode(ModalGraphMouse.Mode.PICKING);
+ }
+
+
+ public void clear() {
+ for (TSState st : new java.util.ArrayList(tsGraph.getVertices())) {
+ tsGraph.removeVertex(st);
+ }
+
+ repaint();
+ }
+
+
+ /** For better vertex placement */
+ private void relax() {
+ graphLayout.initialize();
+ graphLayout.setSize(graphViewer.getSize());
+ Relaxer relaxer = graphViewer.getModel().getRelaxer();
+
+ if (relaxer != null) {
+ relaxer.stop();
+ relaxer.prerelax();
+ relaxer.relax();
+ }
+ }
+
+
+ //---------------------------------------------------------------------------------------------
+ // For drawing the initial state
+ //---------------------------------------------------------------------------------------------
+
+ static class SquareIcon implements Icon {
+ private final Color fillColor;
+ private final int width;
+
+ public SquareIcon(Color fColor, int width) {
+ fillColor = fColor;
+ this.width = width;
+ }
+
+ public void paintIcon(Component c, Graphics g, int x, int y) {
+ g.setColor(fillColor);
+ g.fillRect(x, y, width, width);
+ g.setColor(Color.black);
+ g.drawRect(x, y, width, width);
+ }
+
+ public int getIconWidth() {
+ return width;
+ }
+
+ public int getIconHeight() {
+ return width;
+ }
+ }
+
+
+ //---------------------------------------------------------------------------------------------
+ // For drawing all non-initial states
+ //---------------------------------------------------------------------------------------------
+
+ static class CircleIcon implements Icon {
+ private final Color fillColor;
+ private final int radius;
+
+ public CircleIcon(Color fColor, int radius) {
+ fillColor = fColor;
+ this.radius = radius;
+ }
+
+ public void paintIcon(Component c, Graphics g, int x, int y) {
+ g.setColor(fillColor);
+ g.fillOval(x, y, radius, radius);
+ g.setColor(Color.black);
+ g.drawOval(x, y, radius, radius);
+ }
+
+ public int getIconWidth() {
+ return radius;
+ }
+
+ public int getIconHeight() {
+ return radius;
+ }
+ }
+
+ public void onRSUpdate() {
+ clear();
+ }
+
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Single node of the Transition system graph
+//-------------------------------------------------------------------------------------------------
+
+class TSState {
+
+ public final static Color fillColor = Color.lightGray;
+ public final static Color initialColor = new Color(102, 178, 255);
+
+ private static final int nodeWidth = 30;
+ private static final int nodeHeight = 30;
+
+ private final int id;
+ private final String rsDetails;
+ private final String toolTipText;
+ private final String aState;
+ private boolean initial = false;
+
+ public TSState(int id, String stateStr) {
+ 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() {
+ return initial;
+ }
+
+ public void setAsInitial() {
+ initial = true;
+ }
+
+ public String toString() {
+ return String.valueOf(id);
+ }
+
+ public int getWidth() {
+ return nodeWidth;
+ }
+
+ public int getHeight() {
+ return nodeHeight;
+ }
+
+ Color getFillColor() {
+ return initial ? initialColor : fillColor;
+ }
+
+ public String getTooltipText() {
+ 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) +
+ "";
+ }
+}
+
+
+//-------------------------------------------------------------------------------------------------
+// Single edge of the Transition system graph
+//-------------------------------------------------------------------------------------------------
+
+class TSTransition { }