artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Released version of GUI #5

Merged
Ghost merged 5 commits from refs/pull/5/head into master 2025-06-04 19:21:51 +01:00
Conversation 0 Commits 5 Files Changed 21 +4571 -3
21 changed files with 4571 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

103
reactics-bdd/export.cc
View File

@@ -808,3 +808,106 @@ string RSExporter::formulaToStr(const FormRSCTLK * form) {
return "??";
}
}
void RSExporter::exportToXML() {
output << "<xml version=\"1.0\">\n"
<< indent << "<reaction-system>\n";
for (Process proc=0; proc<rs->getNumberOfProcesses(); ++proc) {
output << indent << indent << "<process name=\"" << rs->processes_ids[proc] << "\">\n";
for (const auto & reaction : rs->proc_reactions[proc]) {
output << indent << indent << indent << "<reaction>\n";
for (const Entity & e : reaction.rctt) {
output << indent << indent << indent << indent
<< "<reactant>" << rs->getEntityName(e) << "</reactant>\n";
}
for (const Entity & e : reaction.inhib) {
output << indent << indent << indent << indent
<< "<inhibitor>" << rs->getEntityName(e) << "</inhibitor>\n";
}
for (const Entity & e : reaction.prod) {
output << indent << indent << indent << indent
<< "<product>" << rs->getEntityName(e) << "</product>\n";
}
output << indent << indent << indent << "</reaction>\n";
}
output << indent << indent << "</process>\n";
}
output << indent << "</reaction-system>\n";
output << indent << "<context-automaton>\n";
for (unsigned stId=0; stId<rs->ctx_aut->states_ids.size(); ++stId) {
if (rs->ctx_aut->states_ids[stId] == "T")
continue;
output << indent << indent << "<state id=\"" << stId + 1 << "\" name=\""
<< rs->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<map<State, vector<CtxAutTransition>>> 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; src<edges.size(); ++src) {
for (const auto &dst : edges[src]) {
output << indent << indent << "<edge from=\"" << rs->ctx_aut->getStateName(src)
<< "\" to=\"" << rs->ctx_aut->getStateName(dst.first) << "\">\n";
for (const CtxAutTransition &trans : dst.second) {
output << indent << indent << indent << "<transition context=\"" << rs->procEntitiesToStr(trans.ctx) << "\"";
if (trans.state_constr)
output << " guard=\"" << trans.state_constr->toStr() << "\"";
output << "/>\n";
}
output << indent << indent << "</edge>\n";
}
}
output << indent << "</context-automaton>\n";
output << indent << "<formulas>\n";
for (const auto & prop : drv->properties) {
string fStr = "";
for (const char ch : prop.second->toStr()) {
if (ch == '<')
fStr += "&lt;";
else if (ch =='>')
fStr += "&gt;";
else
fStr += ch;
}
output << indent << indent << indent << "<formula label=\"" << prop.first <<"\">"
<< fStr << "</formula>\n";
}
output << indent << "</formulas>\n";
output << "</xml>" << endl;
}

2
reactics-bdd/export.hh
View File

@@ -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;

17
reactics-bdd/reactics.cc
View File

@@ -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

BIN
reactics-gui/resources/help/img/ctx-automaton-edge-details.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 7.7 KiB

BIN
reactics-gui/resources/help/img/ctx-automaton-panel.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 3.7 KiB

BIN
reactics-gui/resources/help/img/ctx-automaton-state.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 5.1 KiB

BIN
reactics-gui/resources/help/img/ctx-automaton-transition-edit.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 12 KiB

321
reactics-gui/resources/help/index.html Normal file
View File

@@ -0,0 +1,321 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>ReactICS GUI Help</title>
</head>
<body>
<hr>
<center><a name="top"><h1>ReactICS - Distributed Reaction Systems Model Checker</h1></a></center>
<hr>
<p align="justify">
<b>ReactICS</b> is a toolkit that allows for verification of Reaction Systems.
The toolkit consists of two separate modules implementing:
<ul>
<li>Methods using binary decision diagrams (BDD)
for storing and manipulating the state space of the verified system.</li>
<li>Methods translating the verification problems into satisfiability modulo theories (SMT).</li>
</ul>
</p>
<p align="justify">
<b>ReactICS GUI</b> offers a graphical user interface allowing for editing the reaction system details
and model checking using BDD module.
</p>
<p align="justify">
More on <b>ReactICS</b> can be found at <a href="https://reactics.org">The Reactics Webpage</a>.
</p>
<br/>
<hr/>
<h2>Table of contents</h2>
<ul>
<li><a href="#reaction-systems">Reaction systems</a><br/></li>
<li><a href="#gui">Application functions</a><br/></li>
<li><a href="#rs-edit">Reaction system editor</a><br/></li>
<li><a href="#ctx-edit">Context automaton editor</a><br/></li>
<li><a href="#trs-view">Transition system viewer</a><br/></li>
<li><a href="#model-checking">Model checking</a><br/></li>
</ul>
<br/>
<hr/>
<a name="reaction-systems"><h2>Reaction Systems</h2></a>
<hr/>
<p align="justify">
<b>Reaction Systems</b> 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.
</p>
<p align="justify">
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.
</p>
<p align="justify">
A <b>Distributed Reaction System</b> 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.
</p>
<p align="justify">
More on reaction system can be found at <a href="https://www.reactionsystems.org">The Reaction System Webpage</a>
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<hr/>
<a name="gui"><h2>Application functions</h2></a>
<hr/>
<p align="justify">
<b>ReactICS GUI</b> allows to:
<ul>
<li>Edit the reaction system structure (the number of processes/agents, reactions for each process/agent, etc.)</li>
<li>Edit the context automaton structure (adding/removing states and transitions,
edit context for active processes/agents, setting guards for transitions, etc.). </li>
<li>Preview of the state space represented as a transition system.</li>
<li>Verification of properties defined by formulas using rsCTLK semantics.</li>
<li>Save/load the reaction system structure to/from XML file.</li>
<li>Export/import the reaction system to/from RSSL file.</li>
<li>Export the reaction system structure and behaviour to ISPL file.</li>
</ul>
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<hr/>
<a name="rs-edit"><h2>Distributed reaction system editor</h2></a>
<hr/>
<p align="justify">
The structure of distributed reaction system can be edited using the following buttons from the distributed reaction system control panel:
<center><img src="img/rs-ctrl-buttons.png"/></center>
<ul>
<li><b>New process</b> - Creates a new empty process.</li>
<li><b>Remove</b> - Removes selected processes.</li>
<li><b>Copy</b> - Makes copies of selected processes (together with all reactions).</li>
<li><b>Rename</b> - Renames a selected process. Note that process names should be unique.</li>
<li><b>Move up</b> - Moves selected process up the list of all processes.</li>
<li><b>Move down</b> - Moves selected process down the list of all processes.</li>
</ul>
</p>
<p align="justify">
The details of a single process can be edited using the following buttons in the process panel:
<center><img src="img/process-edit-button.png"/></center>
<ul>
<li><b>Add reaction</b> - Creates a new reaction. The details of the reaction should be specified in dialog shown below.</li>
<li><b>Edit reaction</b> - Allows to edit the details of a selected reaction using dialog shown below.</li>
<li><b>Remove reaction</b> - Removes a selected reaction.</li>
</ul>
</p>
<center><img src="img/reaction-details.png"/></center>
<p align="justify">
Verification of formulas against a system specification is done after selecting desired formulas
and clicking <b>Evaluate</b> button.
The result of the verification (<b>True</b>/<b>False</b>), as well as time and memory used are presented next to each verified formula.
</p>
<center><img src="img/model-checking.png"/></center>
<p align="justify">
Clicking the <b>Reset</b> 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.
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<hr/>
<a name="ctx-edit"><h2>Context automaton editor</h2></a>
<hr/>
<p align="justify">
To create or edit the context automaton structure a proper edit mode should be set using the <b>edit mode panel</b>.
</p>
<br/>
<center><img src="img/ctx-automaton-panel.png"/></center>
<p align="justify">
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).
</p>
<br/>
<h3>States</h3>
<p align="justify">
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.
</p>
<br/>
<center><img src="img/ctx-automaton-state.png"/></center>
<p align="justify">
The details of a state can be edited by right-clicking the existing
state and choosing the right option from the popup menu:
<ul>
<li><b>Set as initial</b> - Makes the selected state the initial state of the context automaton.</li>
<li><b>Set label</b> - Allows to set the custom label for the selected state. Note that state labels have to be unique.</li>
</ul>
</p>
<br/>
<center><img src="img/ctx-automaton-state.png"/></center>
<h3>Edges</h3>
<p align="justify">
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 <i>context</i> (additional entities
provided for active processes/agents) and a <i>guard</i> (a condition required by the transition to execute).
The list of transitions may be edited by right-clicking the existing
edge and choosing the <b>Nondeterministic transitions</b> popup menu.
</p>
<center><img src="img/ctx-automaton-transition-edit.png"/></center>
<p align="justify">
Hovering the mouse above an edge allows to see the full list of transitions
including context and guards.
</p>
<center><img src="img/ctx-automaton-edge-details.png"/></center>
<br/>
<h3>Removing context automaton elements</h3>
<p align="justify">
Switching the toggle button <b>Delete</b> 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 <b>Clear</b> button.
</p>
<br/>
<h3>Transforming the context automaton graph</h3>
<p align="justify">
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 <b>CTRL + left-click</b> on a particular state the entire automaton graph is shifted to be centered
on the clicked state.
Checking the <b>Lock relative nodes positions</b> 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.
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<hr/>
<a name="trs-view"><h2>Transition system viewer</h2></a>
<hr/>
<p align="justify">
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 S<sub>i</sub> to the state S<sub>j</sub>
if S<sub>f</sub> is reachable from S<sub>i</sub> by a single computation step of the reaction system.
</p>
<p align="justify">
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).
</p>
<p align="justify">
Computation is done by pressing <b>Update transition system</b> button.
The reaction system structure should be loaded from the file or edited manually for the computation to be possible.
</p>
<p align="justify">
Note that no matter in which component the <b>Update transition system</b> button
is pressed, the transition system structure will be updated in both.
</p>
<p align="justify">
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).
</p>
<center><img src="img/ctx-automaton-edge-details.png"/></center>
<br/>
<h3>Transforming the transition system graph</h3>
<p align="justify">
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 <b>CTRL + left-click</b> on a particular state the entire transition system graph is shifted to be centered
on the clicked state.
Checking the <b>Lock relative nodes positions</b> 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.
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<hr/>
<a name="model-checking"><h2>Model checking</h2></a>
<hr/>
<p align="justify">
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 <b>rsCTLK</b> syntax.
</p>
<p align="justify">
The list of formulas may be modified using the following buttons:
<ul>
<li><b>Add formula</b> - Creates an empty formula. The details of the formula should be specified in dialog shown below.</li>
<li><b>Edit formula</b> - Allows to edit the details of a selected formula using dialog shown below.</li>
<li><b>Remove formulas</b> - Removes selected formulas.</li>
</ul>
</p>
<center><img src="img/formula-details.png"/></center>
<p align="justify">
Verification of formulas against a system specification is done after selecting desired formulas
and clicking <b>Evaluate</b> button.
The result of the verification (<b>True</b>/<b>False</b>), as well as time and memory used are presented next to each verified formula.
</p>
<center><img src="img/model-checking.png"/></center>
<p align="justify">
Clicking the <b>Reset</b> 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.
</p>
<center><a href="#top">Back to top</a></center>
<br/>
<br/>
</body>
</html>

3
reactics-gui/src/META-INF/MANIFEST.MF Normal file
View File

@@ -0,0 +1,3 @@
Manifest-Version: 1.0
Main-Class: pl.umk.mat.martinp.reactics.ReacticsGUI

693
reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java Normal file
View File

@@ -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<CAState, CAEdge> graphViewer;
private Layout<CAState, CAEdge> 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<EditorModeButton> 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<CAState, CAEdge> autoLayout = new FRLayout<CAState, CAEdge>(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<String> getReactantsSet() { return graph.getReactantsSet(); }
//--------------------------------------------------------------------------
// Creates visualization viewer for context automaton graph display/edition
//--------------------------------------------------------------------------
private void createGraphEditor() {
gLayout = new StaticLayout<CAState, CAEdge>(graph,
new Transformer<CAState, Point2D>() {
public Point2D transform(CAState node) {
return node.getLocation();
}
});
graphViewer = new VisualizationViewer<CAState, CAEdge>(gLayout, initialEditorSize) {
public JToolTip createToolTip() {
JToolTip tooltip = super.createToolTip();
tooltip.setFont(toolTipFont);
return tooltip;
}
};
// Nodes labels
graphViewer.getRenderContext().setVertexLabelTransformer(
new ToStringLabeller<CAState>());
graphViewer.getRenderer().getVertexLabelRenderer()
.setPosition(Renderer.VertexLabel.Position.CNTR);
graphViewer.getRenderContext().setVertexFontTransformer(
new Transformer<CAState,Font>() {
public Font transform(CAState v) {
return nodeLabelFont;
}
});
// Nodes colour, background, etc.
graphViewer.getRenderContext().setVertexIconTransformer(new Transformer<CAState,Icon>() {
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<CAEdge, Paint>() {
public Paint transform(CAEdge e) {
return edgeColor;
}
});
graphViewer.getRenderContext().setEdgeStrokeTransformer(new Transformer<CAEdge, Stroke>() {
public Stroke transform(CAEdge e) {
return basicEdgeStroke;
}
});
graphViewer.getRenderContext().setEdgeArrowStrokeTransformer(new Transformer<CAEdge, Stroke>() {
public Stroke transform(CAEdge e) {
return basicEdgeArrow;
}
});
graphViewer.getRenderContext().setArrowFillPaintTransformer(new Transformer<CAEdge, Paint>() {
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<CAEdge>());
graphViewer.getRenderContext().getEdgeLabelRenderer().setRotateEdgeLabels(true);
graphViewer.getRenderContext().setLabelOffset(20);
graphViewer.getRenderContext().setEdgeFontTransformer(new Transformer<CAEdge, Font>() {
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<CAState, String>() {
public String transform(CAState caState) {
return caState.getTooltipText();
}
});
graphViewer.setEdgeToolTipTransformer(new Transformer<CAEdge, String>() {
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<EditorModeButton>();
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<modeButtons.size();++i)
modeButtons.elementAt(i).addActionListener(mbListener);
JPanel btnPanel = new JPanel();
btnPanel.setLayout(new FlowLayout());
for(int i=0;i<modeButtons.size();++i)
btnPanel.add(modeButtons.elementAt(i));
JCheckBox posLockCBox = new JCheckBox("Lock relative nodes positions");
posLockCBox.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent actionEvent) {
lockNodesPositions(posLockCBox.isSelected());
}
});
btnPanel.add(posLockCBox);
add(btnPanel,BorderLayout.NORTH);
}
//---------------------------------------------------------------
// Create context menus for transitions, places and edges
//---------------------------------------------------------------
private void createContextMenus() {
stateContextMenu = new JPopupMenu();
JMenuItem stateInitialItem = new JMenuItem("Set as initial");
stateInitialItem.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent e) {
PickedState<CAState> pickedVertexState = graphViewer.getPickedVertexState();
Set<CAState> pickedNodes = pickedVertexState.getPicked();
Iterator<CAState> 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<CAState> pickedVertexState = graphViewer.getPickedVertexState();
Set<CAState> pickedNodes = pickedVertexState.getPicked();
Iterator<CAState> 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<CAEdge> pickedEdgeState = graphViewer.getPickedEdgeState();
Set<CAEdge> pickedEdges = pickedEdgeState.getPicked();
Iterator<CAEdge> 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,
"<html>State label should start with a letter and may contain only:<br/>" +
"letters, numbers, colons (:), underscores (_) and hyphens (-)</html>",
"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<CAState> 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<CAState> nodes = graph.getVertices();
for(CAState n : nodes) {
n.updateLocation(gLayout.transform(n));
}
}
/** For better vertex placement */
private void relax() {
Layout<CAState, CAEdge> 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<modeButtons.size();++i)
if(i != num || emb.mode == EditorState.CLEAR)
modeButtons.elementAt(i).setSelected(false);
edtState = emb.getMode();
}
else {
edtState = EditorState.NONE;
}
if (edtState == EditorState.CLEAR) {
graph.clear();
repaint();
edtState = EditorState.NONE;
}
}
};
//---------------------------------------------------------------------------------------------
// Mouse event handler. To allow interactive net editing
//---------------------------------------------------------------------------------------------
class EditorMouseListener extends MouseAdapter {
public void mouseClicked(MouseEvent me) {
int btnClicked = me.getButton();
if(btnClicked == MouseEvent.BUTTON1)
leftButtonClicked(me);
else if(btnClicked == MouseEvent.BUTTON3)
rightButtonClicked(me);
}
private void leftButtonClicked(MouseEvent me) {
Point clickPt = me.getPoint();
GraphElementAccessor<CAState, CAEdge> pickSupport = null;
Layout<CAState, CAEdge> 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<CAState> 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<CAEdge> 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<CAState, CAEdge> pickSupport = graphViewer.getPickSupport();
Layout<CAState, CAEdge> 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<CAState> pickedVertexState = graphViewer.getPickedVertexState();
pickedVertexState.clear();
pickedVertexState.pick(node,true);
stateContextMenu.show(graphViewer, me.getX(), me.getY());
}
else if (edge != null) {
PickedState<CAEdge> 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<V, E> implements Transformer<Context<Graph<V, E>, E>, Shape> {
private final EdgeShape.Loop<V, E> loopShape;
private final Transformer<Context<Graph<V, E>, 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<Graph<V, E>, E> context) {
Graph<V, E> 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);
}
}
}

438
reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java Normal file
View File

@@ -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<CAState, CAEdge> {
private static final long serialVersionUID = 1L;
HashMap<Integer, CAState> 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<CAState> allStates = states.values();
Iterator<CAState> 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(" <context-automaton>");
for (CAState state : states.values()) {
Point2D pos = state.getLocation();
output.print(" <state");
output.print(" id=\"" + state.getId() + "\"");
output.print(" name=\"" + state.getLabel() + "\"");
output.print(" x=\"" + pos.getX() + "\"");
output.print(" y=\"" + pos.getY() + "\"");
if (state.isInitial())
output.print(" initial=\"true\"");
output.println("/>");
}
for (CAEdge edge : edges.keySet()) {
Pair<CAState> endPts = this.getEndpoints(edge);
output.print(" <edge");
output.print(" from=\"" + endPts.getFirst().getLabel() + "\"");
output.print(" to=\"" + endPts.getSecond().getLabel() + "\"");
output.println(">");
for (Transition tr : edge.getTransitions()) {
output.print(" <transition");
output.print(" context=\"" + tr.context + "\"");
output.print(" guard=\"" + tr.guard + "\"");
output.println("/>");
}
output.println(" </edge>");
}
output.println(" </context-automaton>");
}
/**
* 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 <b>inputFile</b> 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<String, CAState> states = new HashMap<String, CAState>();
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<Transition> transitionList = new Vector<Transition>();
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<String> getReactantsSet() {
Set<String> reactants = new HashSet<String>();
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<Transition> 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 "<html>"+
"<b>State</b> " + id + "<br/><hr>" + getLabel() + //"<hr>"+
"</html>";
}
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<Transition> transitions = new Vector<Transition>();
public boolean hasTransition() { return transitions.size() > 0; }
public CAEdge() {
this.id = nextId++;
}
// public CAEdge(Collection<Transition> transitionList) {
// this.transitions.addAll(transitionList);
// }
Vector<Transition> 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("<html><hr/><center><b>Context <font color=\"red\">:</font> Guard</b></center><hr/>");
for (Transition tr : transitions) {
tooTip.append(tr.context).append(" <b><font color=\"red\">:</font></b> ").append(tr.guard).append("<br/><hr/>");
}
tooTip.append("</html>");
return tooTip.toString();
}
public void addTransitions(Collection<Transition> 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);
}
}

13
reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java Normal file
View File

@@ -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);
}
}

410
reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java Normal file
View File

@@ -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<Formula> 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(" <formulas>");
for (Formula f : formulaList)
output.println(" " + f.toXMLString());
output.println(" </formulas>");
}
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("<html>A unique label of the formula</html>");
formulaInput.setToolTipText("<html>Formula to be evaluated</html>");
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<Formula> getSelectedFormulas() {
Vector<Formula> selected = new Vector<Formula>();
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 label=\"" + label +"\">" +
formula.replaceAll("<", "&lt;").replaceAll(">", "&gt;") +
"</formula>";
}
}

125
reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java Normal file
View File

@@ -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("<html><h1>" + ReacticsGUI.ApplicationName + "</h1>"
+ "<h2>version " + ReacticsGUI.ApplicationVersion + " (" + ReacticsGUI.ApplicationReleaseDate + ")</h2>"
+ "<h3>Model Checker for Reaction Systems</h3>"
+ "<h3>ReactICS Research Team (CC BY 4.0)</h3>"
+ "<h3><a href=\"https://reactics.org\">https://reactics.org</a></h3></html>"));
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);
}
}

427
reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java Normal file
View File

@@ -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("<html>Space separated list of reactants</html>");
inhibitorsInput.setToolTipText("<html>Space separated list of inhibitors</html>");
productsInput.setToolTipText("<html>Space separated list of products</html>");
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<String> reactantsSet = new HashSet<String>(Arrays.asList(reactantsStr.trim().split("\\s+")));
HashSet<String> inhibitorsSet = new HashSet<String>(Arrays.asList(inhibitorsStr.trim().split("\\s+")));
HashSet<String> productsSet = new HashSet<String>(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<String> getReactantsSet() {
HashSet<String> rset = new HashSet<String>();
for (Reaction rr : rsProcess.reactions)
rset.addAll(rr.getReactantsSet());
return rset;
}
public void exportToXML(PrintWriter output) {
output.println(" <process name=\"" + rsProcess.label + "\">");
for (Reaction rr : rsProcess.reactions)
rr.exportToXML(output);
output.println(" </process>");
}
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<String>[] 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<String> reactants;
LinkedList<String> inhibitors;
LinkedList<String> products;
public Reaction() {
reactants = new LinkedList<String>();
inhibitors = new LinkedList<String>();
products = new LinkedList<String>();
}
public Reaction(Reaction rr) {
reactants = new LinkedList<String>(rr.reactants);
inhibitors = new LinkedList<String>(rr.inhibitors);
products = new LinkedList<String>(rr.products);
}
public Set<String> getReactantsSet() {
Set<String> rset = new HashSet<String>();
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(" <reaction>");
for (String str : reactants)
output.println(" <reactant>" + str + "</reactant>");
for (String str : inhibitors)
output.println(" <inhibitor>" + str + "</inhibitor>");
for (String str : products)
output.println(" <product>" + str + "</product>");
output.println(" </reaction>");
}
}

49
reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java Normal file
View File

@@ -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<String> 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());
}
}

791
reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java Normal file
View File

@@ -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("<html><center>Update<br>Reaction System</center></html>");
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<String> rset = new TreeSet<String>();
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<Formula> 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("<xml version=\"1.0\">");
reactionSystemEditor.exportToXML(xmlOut);
contextAutomatonEditor.exportToXML(xmlOut);
formulaEditor.exportToXML(xmlOut);
xmlOut.println("</xml>");
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);
}
}

198
reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java Normal file
View File

@@ -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);
}
}

409
reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java Normal file
View File

@@ -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<ProcessEditor> procEditors = new Vector<ProcessEditor>();
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<String> getReactantsSet() {
HashSet<String> rset = new HashSet<String>();
for (ProcessEditor pe : procEditors)
rset.addAll(pe.getReactantsSet());
return rset;
}
public void exportToXML(PrintWriter output) {
output.println(" <reaction-system>");
for (ProcessEditor process : procEditors)
process.exportToXML(output);
output.println(" </reaction-system>");
}
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<processList.getLength(); ++idx) {
Node processNode = processList.item(idx);
if (processNode.getNodeType() != Node.ELEMENT_NODE)
continue;
String procName = processNode.getAttributes().getNamedItem("name").getNodeValue();
ProcessEditor processEditor = new ProcessEditor(rs.createProcess(procName));
//----------------------------------------------------------------------------------------------------------
// Reactions details
//----------------------------------------------------------------------------------------------------------
NodeList reactionList = processNode.getChildNodes();
for (int rIdx=0; rIdx<reactionList.getLength(); ++rIdx) {
Node reactionNode = reactionList.item(rIdx);
if (reactionNode.getNodeType() != Node.ELEMENT_NODE)
continue;
Reaction reaction = new Reaction();
NodeList substrateNodes = reactionNode.getChildNodes();
for (int sIdx=0; sIdx<substrateNodes.getLength(); ++sIdx) {
Node sNode = substrateNodes.item(sIdx);
if (sNode.getNodeType() != Node.ELEMENT_NODE)
continue;
String nodeName = sNode.getNodeName();
String nodeContent = sNode.getTextContent();
switch (nodeName) {
case "reactant":
reaction.reactants.add(nodeContent);
break;
case "inhibitor":
reaction.inhibitors.add(nodeContent);
break;
case "product":
reaction.products.add(nodeContent);
break;
default:
throw new ReactionSystemStructureError("Unexpected node type: " + nodeName);
}
}
processEditor.addReaction(reaction);
}
procEditors.add(processEditor);
processPanel.add(processEditor);
}
revalidate();
}
public String toRSSLString() {
StringBuilder rsString = new StringBuilder("reactions {\n");
for (ProcessEditor pe : procEditors) {
rsString.append(pe.toRSSLString());
}
rsString.append("};\n");
return rsString.toString();
}
public void clear() {
processPanel.removeAll();
procEditors.clear();
rs.clearProcesses();
}
private void createProcess() {
ProcessEditor newProcEdt = new ProcessEditor(rs.createProcess());
procEditors.add(newProcEdt);
processPanel.add(newProcEdt);
rs.modified = true;
revalidate();
}
private void createProcess(String label) {
ProcessEditor newProcEdt = new ProcessEditor(rs.createProcess(label));
procEditors.add(newProcEdt);
processPanel.add(newProcEdt);
rs.modified = true;
revalidate();
}
private void removeProcesses() {
Vector<ProcessEditor> toRemove = new Vector<ProcessEditor>();
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<ProcessEditor> toBeCopied = new Vector<ProcessEditor>();
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,
"<html>Process name should start with a letter and may contain only:<br/>" +
"letters, numbers, colons (:), underscores (_) and hyphens (-)</html>",
"Error", JOptionPane.ERROR_MESSAGE);
}
else {
idOk = true;
rs.renameProcess(toRename.getProcess(), newLabel);
toRename.rename(newLabel);
rs.notifyObservers();
}
}
while (!idOk);
}
private void moveSelectedUp() {
Vector<Integer> toBeMovedIds = new Vector<Integer>();
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<Integer> toBeMovedIds = new Vector<Integer>();
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);
}
}

208
reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java Normal file
View File

@@ -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<Transition> 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<Transition> trans, String from, String to) {
setTitle("Transitions for (" + from + " -> " + to + ")");
transitions = (Vector<Transition>) 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("<html>Additional entities for processes</html>");
guardInput.setToolTipText("<html>Initial conditions for the transition in rsCTL format.</html>");
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;
}
}
}

367
reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java Normal file
View File

@@ -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<TSState, TSTransition> graphViewer;
private Layout<TSState, TSTransition> graphLayout;
DefaultModalGraphMouse graphMouse;
//---------------------------------------------------------------
// Transition system graph
//---------------------------------------------------------------
private DirectedSparseGraph<TSState, TSTransition> 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<TSState, TSTransition>();
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<TSState, TSTransition>(tsGraph);
graphViewer = new VisualizationViewer<TSState, TSTransition>(graphLayout, initialEditorSize) {
public JToolTip createToolTip() {
JToolTip tooltip = super.createToolTip();
tooltip.setFont(toolTipFont);
return tooltip;
}
};
// Nodes labels
graphViewer.getRenderContext().setVertexLabelTransformer(
new ToStringLabeller<TSState>());
graphViewer.getRenderer().getVertexLabelRenderer()
.setPosition(Renderer.VertexLabel.Position.CNTR);
graphViewer.getRenderContext().setVertexFontTransformer(
new Transformer<TSState,Font>() {
public Font transform(TSState st) {
return nodeLabelFont;
}
});
// Nodes colour, background, etc.
graphViewer.getRenderContext().setVertexIconTransformer(new Transformer<TSState,Icon>() {
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<TSTransition, Stroke>() {
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<TSState, String>() {
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<String, TSState> 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<TSState>(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+=\\{)", "}<br/>$1");
}
private String formatToolTipText() {
Pattern pattern = Pattern.compile("\\w+=\\{[^}]*\\}");
Matcher matcher = pattern.matcher(rsDetails);
ArrayList<String> blocks = new ArrayList<String>();
while (matcher.find()) {
blocks.add(matcher.group());
}
if (aState != null)
return "<html>" +
"<b>CA</b> " + aState+ "<br/><hr>" +
String.join("<br/>", blocks) +
"</html>";
else
return "<html>" +
String.join("<br/>", blocks) +
"</html>";
}
}
//-------------------------------------------------------------------------------------------------
// Single edge of the Transition system graph
//-------------------------------------------------------------------------------------------------
class TSTransition { }