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

Automatic update of the reactants set panel + help content.

Browse Source
This commit is contained in:
Marcin Piątkowski
2025-06-04 11:33:37 +02:00
parent 8e7ea9dd96
commit dbeb235c50
6 changed files with 82 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

68
reactics-gui/resources/help/index.html
View File

@@ -7,7 +7,7 @@
<body>
<hr>
<center><a name="top"><h1>ReactICS - Reaction Systems Model Checker</h1></a></center>
<center><a name="top"><h1>ReactICS - Distributed Reaction Systems Model Checker</h1></a></center>
<hr>
@@ -97,13 +97,47 @@
<hr/>
<a name="rs-edit"><h2>Reaction system editor</h2></a>
<a name="rs-edit"><h2>Distributed reaction system editor</h2></a>
<hr/>
<p align=""justify">
<b>-- TODO --</b>
<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/>
@@ -253,8 +287,30 @@
<a name="model-checking"><h2>Model checking</h2></a>
<hr/>
<p align=""justify">
<b>-- TODO --</b>
<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>

1
reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java
View File

@@ -384,6 +384,7 @@ public class ContextAutomatonEditor extends JPanel implements RSObserver {
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).

4
reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java
View File

@@ -7,7 +7,6 @@ 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";
@@ -49,6 +48,9 @@ public class HelpWindow extends JFrame {
try {
URL helpUrl = this.getClass().getResource(docPath + startDocument);
helpPane.setPage(helpUrl);
helpPane.revalidate();
helpPane.repaint();
}
catch (Exception e) {
System.out.println("Exception: " + e.getMessage());

6
reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java
View File

@@ -23,6 +23,7 @@ class ProcessEditor extends JPanel {
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);
@@ -107,6 +108,8 @@ class ProcessEditor extends JPanel {
add(new JScrollPane(reactionList));
setPreferredSize(new Dimension(-1, 200));
rs = ReactionSystem.getInstance();
}
private boolean showReactionEditDialog(JComponent parent, Reaction rr) {
@@ -280,6 +283,7 @@ class ProcessEditor extends JPanel {
rsProcess.reactions.add(rr);
modified = true;
reactionsModel.fireTableDataChanged();
rs.notifyObservers();
}
// Edit details of an existing reaction
@@ -300,6 +304,7 @@ class ProcessEditor extends JPanel {
rsProcess.reactions.setElementAt(rr, rIdx);
modified = true;
reactionsModel.fireTableDataChanged();
rs.notifyObservers();
}
// Remove an existing reaction
@@ -316,6 +321,7 @@ class ProcessEditor extends JPanel {
reactionsModel.fireTableDataChanged();
modified = true;
this.repaint();
rs.notifyObservers();
}
private void toggleSelection() {

11
reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java
View File

@@ -5,9 +5,10 @@ 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 {
public class ReactantSetPanel extends JPanel implements RSObserver {
private final int borderThickness = 2;
JTextArea textArea = new JTextArea();
@@ -33,10 +34,16 @@ public class ReactantSetPanel extends JPanel {
public void updateReactants(Set<String> reactantsSet) {
textArea.setText("");
textArea.setText(Arrays.toString(reactantsSet.toArray()));
// 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());
}
}

2
reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java
View File

@@ -314,6 +314,7 @@ public class ReacticsGUI extends JFrame {
buttonPanel.add(updateButton);
topPanel.add(buttonPanel, BorderLayout.WEST);
reactantSetPanel = new ReactantSetPanel();
reactionSystem.addObserver(reactantSetPanel);
topPanel.add(reactantSetPanel, BorderLayout.CENTER);
getContentPane().add(topPanel, BorderLayout.NORTH);
}
@@ -672,7 +673,6 @@ public class ReacticsGUI extends JFrame {
outStream.println("options { use-context-automaton; make-progressive; };\n");
outStream.println(reactionSystemEditor.toRSSLString());
outStream.println(contextAutomatonEditor.toRSSLString());
// outStream.println(formulaEditor.toRSSLString());
}
private void showAboutWindow() {