Merge lp:~danilovesky/workcraft/trunk-circuit-env-stg into lp:workcraft
- trunk-circuit-env-stg
- Merge into trunk
Proposed by
Danil Sokolov
Status: | Merged |
---|---|
Merged at revision: | 501 |
Proposed branch: | lp:~danilovesky/workcraft/trunk-circuit-env-stg |
Merge into: | lp:workcraft |
Diff against target: |
2369 lines (+815/-640) 39 files modified
CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java (+60/-16) CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java (+21/-0) CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java (+55/-47) CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java (+2/-1) CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java (+8/-4) CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java (+0/-111) CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java (+0/-110) CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java (+213/-68) CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java (+0/-43) CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java (+0/-43) CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java (+15/-3) CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java (+20/-23) CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java (+3/-1) DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java (+1/-9) DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java (+15/-8) DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java (+15/-8) DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java (+16/-10) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java (+44/-37) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java (+2/-2) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java (+127/-17) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java (+15/-7) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java (+32/-0) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java (+22/-0) MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java (+1/-1) MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java (+1/-1) MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java (+28/-23) MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java (+4/-4) MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java (+2/-2) MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java (+3/-1) PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java (+15/-8) STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java (+1/-1) STGPlugin/src/org/workcraft/plugins/stg/STG.java (+3/-8) STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java (+0/-7) WorkcraftCore/src/org/workcraft/dom/AbstractModel.java (+9/-1) WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java (+0/-3) WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java (+4/-0) WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java (+19/-0) WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java (+22/-0) WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java (+17/-12) |
To merge this branch: | bzr merge lp:~danilovesky/workcraft/trunk-circuit-env-stg |
Related bugs: | |
Related blueprints: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Danil Sokolov | Approve | ||
Review via email:
|
Commit message
Description of the change
To post a comment you must log in.
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Danil Sokolov (danilovesky) : | # |
review:
Approve
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java' |
2 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java 2013-09-17 14:58:15 +0000 |
3 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java 2014-04-29 16:24:51 +0000 |
4 | @@ -9,8 +9,6 @@ |
5 | import org.workcraft.gui.propertyeditor.SettingsPage; |
6 | import org.workcraft.plugins.circuit.serialisation.FunctionDeserialiser; |
7 | import org.workcraft.plugins.circuit.serialisation.FunctionSerialiser; |
8 | -import org.workcraft.plugins.circuit.tools.CheckCircuitDeadlockTool; |
9 | -import org.workcraft.plugins.circuit.tools.CheckCircuitHazardTool; |
10 | import org.workcraft.plugins.circuit.tools.CheckCircuitTool; |
11 | import org.workcraft.plugins.circuit.tools.STGGeneratorTool; |
12 | import org.workcraft.serialisation.xml.XMLDeserialiser; |
13 | @@ -34,20 +32,6 @@ |
14 | return new STGGeneratorTool(framework); |
15 | } |
16 | }); |
17 | - |
18 | - pm.registerClass(Tool.class, new Initialiser<Tool>() { |
19 | - @Override |
20 | - public Tool create() { |
21 | - return new CheckCircuitDeadlockTool(framework); |
22 | - } |
23 | - }); |
24 | - |
25 | - pm.registerClass(Tool.class, new Initialiser<Tool>() { |
26 | - @Override |
27 | - public Tool create() { |
28 | - return new CheckCircuitHazardTool(framework); |
29 | - } |
30 | - }); |
31 | |
32 | pm.registerClass(Tool.class, new Initialiser<Tool>() { |
33 | @Override |
34 | @@ -56,6 +40,66 @@ |
35 | } |
36 | }); |
37 | |
38 | + pm.registerClass(Tool.class, new Initialiser<Tool>() { |
39 | + @Override |
40 | + public Tool create() { |
41 | + return new CheckCircuitTool(framework) { |
42 | + @Override |
43 | + public String getDisplayName() { |
44 | + return "Check circuit only for conformation"; |
45 | + } |
46 | + @Override |
47 | + public boolean checkDeadlock() { |
48 | + return false; |
49 | + } |
50 | + @Override |
51 | + public boolean checkHazard() { |
52 | + return false; |
53 | + } |
54 | + }; |
55 | + } |
56 | + }); |
57 | + |
58 | + pm.registerClass(Tool.class, new Initialiser<Tool>() { |
59 | + @Override |
60 | + public Tool create() { |
61 | + return new CheckCircuitTool(framework) { |
62 | + @Override |
63 | + public String getDisplayName() { |
64 | + return "Check circuit only for deadlocks"; |
65 | + } |
66 | + @Override |
67 | + public boolean checkConformation() { |
68 | + return false; |
69 | + } |
70 | + @Override |
71 | + public boolean checkHazard() { |
72 | + return false; |
73 | + } |
74 | + }; |
75 | + } |
76 | + }); |
77 | + |
78 | + pm.registerClass(Tool.class, new Initialiser<Tool>() { |
79 | + @Override |
80 | + public Tool create() { |
81 | + return new CheckCircuitTool(framework) { |
82 | + @Override |
83 | + public String getDisplayName() { |
84 | + return "Check circuit only for hazards"; |
85 | + } |
86 | + @Override |
87 | + public boolean checkConformation() { |
88 | + return false; |
89 | + } |
90 | + @Override |
91 | + public boolean checkDeadlock() { |
92 | + return false; |
93 | + } |
94 | + }; |
95 | + } |
96 | + }); |
97 | + |
98 | pm.registerClass(ModelDescriptor.class, CircuitModelDescriptor.class); |
99 | pm.registerClass(XMLSerialiser.class, FunctionSerialiser.class); |
100 | pm.registerClass(XMLDeserialiser.class, FunctionDeserialiser.class); |
101 | |
102 | === added file 'CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java' |
103 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java 1970-01-01 00:00:00 +0000 |
104 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java 2014-04-29 16:24:51 +0000 |
105 | @@ -0,0 +1,21 @@ |
106 | +package org.workcraft.plugins.circuit; |
107 | + |
108 | +import java.io.File; |
109 | + |
110 | +import org.workcraft.dom.math.MathNode; |
111 | + |
112 | +public class Environment extends MathNode { |
113 | + private File file; |
114 | + |
115 | + public Environment() { |
116 | + |
117 | + } |
118 | + |
119 | + public File getFile() { |
120 | + return file; |
121 | + } |
122 | + |
123 | + public void setFile(File file) { |
124 | + this.file = file; |
125 | + } |
126 | +} |
127 | |
128 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java' |
129 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java 2014-04-09 22:33:19 +0000 |
130 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java 2014-04-29 16:24:51 +0000 |
131 | @@ -37,6 +37,7 @@ |
132 | import org.workcraft.exceptions.VisualModelInstantiationException; |
133 | import org.workcraft.gui.propertyeditor.Properties; |
134 | import org.workcraft.plugins.circuit.Contact.IOType; |
135 | +import org.workcraft.serialisation.xml.NoAutoSerialisation; |
136 | import org.workcraft.util.Hierarchy; |
137 | |
138 | |
139 | @@ -45,10 +46,9 @@ |
140 | public class VisualCircuit extends AbstractVisualModel { |
141 | |
142 | private Circuit circuit; |
143 | - private File environmentFile; |
144 | |
145 | @Override |
146 | - public void validateConnection(Node first, Node second) throws InvalidConnectionException { |
147 | + public void validateConnection(Node first, Node second) throws InvalidConnectionException { |
148 | if (first==second) { |
149 | throw new InvalidConnectionException ("Connections are only valid between different objects"); |
150 | } |
151 | @@ -77,24 +77,12 @@ |
152 | } |
153 | } |
154 | |
155 | -/* |
156 | - private final class StateSupervisorExtension extends StateSupervisor { |
157 | - @Override |
158 | - public void handleEvent(StateEvent e) { |
159 | -// if(e instanceof PropertyChangedEvent) |
160 | - |
161 | - } |
162 | - } |
163 | -*/ |
164 | - |
165 | - public VisualCircuit(Circuit model, VisualGroup root) |
166 | - { |
167 | + public VisualCircuit(Circuit model, VisualGroup root) { |
168 | super(model, root); |
169 | circuit=model; |
170 | } |
171 | |
172 | - public VisualCircuit(Circuit model) |
173 | - throws VisualModelInstantiationException { |
174 | + public VisualCircuit(Circuit model) throws VisualModelInstantiationException { |
175 | super(model); |
176 | circuit=model; |
177 | try { |
178 | @@ -102,13 +90,10 @@ |
179 | } catch (NodeCreationException e) { |
180 | throw new VisualModelInstantiationException(e); |
181 | } |
182 | - |
183 | - //new StateSupervisorExtension().attach(getRoot()); |
184 | } |
185 | |
186 | @Override |
187 | - public void connect(Node first, Node second) |
188 | - throws InvalidConnectionException { |
189 | + public void connect(Node first, Node second) throws InvalidConnectionException { |
190 | validateConnection(first, second); |
191 | |
192 | if (first instanceof VisualComponent && second instanceof VisualComponent) { |
193 | @@ -121,6 +106,56 @@ |
194 | nearestAncestor.add(connection); |
195 | } |
196 | } |
197 | + |
198 | + public VisualFunctionContact getOrCreateOutput(String name, double x, double y) { |
199 | + for(VisualFunctionContact c : Hierarchy.filterNodesByType( |
200 | + getRoot().getChildren(), VisualFunctionContact.class)) { |
201 | + if(c.getName().equals(name)) return c; |
202 | + } |
203 | + VisualFunctionContact vc = new VisualFunctionContact(new FunctionContact(IOType.OUTPUT)); |
204 | + vc.setPosition(new Point2D.Double(x, y)); |
205 | + addFunctionContact(vc); |
206 | + vc.setName(name); |
207 | + return vc; |
208 | + } |
209 | + |
210 | + public void addFunctionComponent(VisualFunctionComponent component) { |
211 | + for (Node node : component.getMathReferences()) { |
212 | + circuit.add(node); |
213 | + } |
214 | + super.add(component); |
215 | + } |
216 | + |
217 | + public void addJoint(VisualJoint joint) { |
218 | + for (Node node : joint.getMathReferences()) { |
219 | + circuit.add(node); |
220 | + } |
221 | + super.add(joint); |
222 | + } |
223 | + |
224 | + public void addFunctionContact(VisualFunctionContact contact) { |
225 | + circuit.add(contact.getFunction()); |
226 | + super.add(contact); |
227 | + } |
228 | + |
229 | + @NoAutoSerialisation |
230 | + public File getEnvironmentFile() { |
231 | + File result = null; |
232 | + for (Environment env: Hierarchy.filterNodesByType(getRoot().getChildren(), Environment.class)) { |
233 | + result = env.getFile(); |
234 | + } |
235 | + return result; |
236 | + } |
237 | + |
238 | + @NoAutoSerialisation |
239 | + public void setEnvironmentFile(File value) { |
240 | + for (Environment env: Hierarchy.filterNodesByType(getRoot().getChildren(), Environment.class)) { |
241 | + remove(env); |
242 | + } |
243 | + Environment env = new Environment(); |
244 | + env.setFile(value); |
245 | + add(env); |
246 | + } |
247 | |
248 | @Override |
249 | public Properties getProperties(Node node) { |
250 | @@ -138,31 +173,4 @@ |
251 | return properties; |
252 | } |
253 | |
254 | - public VisualFunctionContact getOrCreateOutput(String name, double x, double y) { |
255 | - |
256 | - for(VisualFunctionContact c : Hierarchy.filterNodesByType(getRoot().getChildren(), VisualFunctionContact.class)) { |
257 | - if(c.getName().equals(name)) return c; |
258 | - } |
259 | - |
260 | - FunctionContact fc = new FunctionContact(IOType.OUTPUT); |
261 | - VisualFunctionContact vc = new VisualFunctionContact(fc); |
262 | - Point2D p2d = new Point2D.Double(); |
263 | - p2d.setLocation(x,y); |
264 | - vc.setPosition(p2d); |
265 | - circuit.add(fc); |
266 | - this.add(vc); |
267 | - |
268 | - vc.setName(name); |
269 | - |
270 | - return vc; |
271 | - } |
272 | - |
273 | - public File getEnvironmentFile() { |
274 | - return environmentFile; |
275 | - } |
276 | - |
277 | - public void setEnvironmentFile(File value) { |
278 | - this.environmentFile = value; |
279 | - } |
280 | - |
281 | } |
282 | |
283 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java' |
284 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java 2014-01-15 14:11:43 +0000 |
285 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java 2014-04-29 16:24:51 +0000 |
286 | @@ -375,7 +375,8 @@ |
287 | public static boolean isDriver(Node contact) { |
288 | if (!(contact instanceof VisualContact)) return false; |
289 | |
290 | - return (((VisualContact)contact).getIOType() == IOType.OUTPUT) == (((VisualContact)contact).getParent() instanceof VisualComponent); |
291 | + return (((VisualContact)contact).getIOType() == IOType.OUTPUT) |
292 | + == (((VisualContact)contact).getParent() instanceof VisualComponent); |
293 | } |
294 | |
295 | |
296 | |
297 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java' |
298 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java 2014-04-09 17:11:48 +0000 |
299 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java 2014-04-29 16:24:51 +0000 |
300 | @@ -89,16 +89,18 @@ |
301 | } |
302 | |
303 | FormulaRenderingResult getRenderedSetFormula(FontRenderContext fcon) { |
304 | - if (renderedSetFormula == null) { |
305 | + if (((FunctionContact)getReferencedContact()).getSetFunction() == null) { |
306 | + return null; |
307 | + } else if (renderedSetFormula == null) { |
308 | renderedSetFormula = FormulaToGraphics.render(((FunctionContact)getReferencedContact()).getSetFunction(), fcon, font); |
309 | } |
310 | return renderedSetFormula; |
311 | } |
312 | |
313 | FormulaRenderingResult getRenderedResetFormula(FontRenderContext fcon) { |
314 | - if (((FunctionContact)getReferencedContact()).getResetFunction()==null) return null; |
315 | - |
316 | - if (renderedResetFormula == null) { |
317 | + if (((FunctionContact)getReferencedContact()).getResetFunction() == null) { |
318 | + return null; |
319 | + } else if (renderedResetFormula == null) { |
320 | renderedResetFormula = FormulaToGraphics.render(((FunctionContact)getReferencedContact()).getResetFunction(), fcon, font); |
321 | } |
322 | return renderedResetFormula; |
323 | @@ -154,6 +156,8 @@ |
324 | |
325 | |
326 | private void drawFormula(Graphics2D g, int arrowType, float xOffset, float yOffset, Color foreground, Color background, FormulaRenderingResult result) { |
327 | + if (result == null) return; |
328 | + |
329 | Rectangle2D textBB = result.boundingBox; |
330 | float textX = 0; |
331 | float textY = (float)-textBB.getCenterY()-(float)0.5-yOffset; |
332 | |
333 | === removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java' |
334 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java 2014-04-16 21:55:15 +0000 |
335 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java 1970-01-01 00:00:00 +0000 |
336 | @@ -1,111 +0,0 @@ |
337 | -package org.workcraft.plugins.circuit.tasks; |
338 | - |
339 | -import java.io.File; |
340 | - |
341 | -import org.workcraft.Framework; |
342 | -import org.workcraft.interop.Exporter; |
343 | -import org.workcraft.plugins.circuit.VisualCircuit; |
344 | -import org.workcraft.plugins.circuit.tools.STGGenerator; |
345 | -import org.workcraft.plugins.mpsat.MpsatMode; |
346 | -import org.workcraft.plugins.mpsat.MpsatResultParser; |
347 | -import org.workcraft.plugins.mpsat.MpsatSettings; |
348 | -import org.workcraft.plugins.mpsat.MpsatUtilitySettings; |
349 | -import org.workcraft.plugins.mpsat.tasks.MpsatChainResult; |
350 | -import org.workcraft.plugins.mpsat.tasks.MpsatChainTask; |
351 | -import org.workcraft.plugins.mpsat.tasks.MpsatTask; |
352 | -import org.workcraft.plugins.mpsat.tasks.PunfTask; |
353 | -import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
354 | -import org.workcraft.plugins.stg.STGModel; |
355 | -import org.workcraft.serialisation.Format; |
356 | -import org.workcraft.tasks.ProgressMonitor; |
357 | -import org.workcraft.tasks.Result; |
358 | -import org.workcraft.tasks.Result.Outcome; |
359 | -import org.workcraft.tasks.SubtaskMonitor; |
360 | -import org.workcraft.util.Export; |
361 | -import org.workcraft.util.Export.ExportTask; |
362 | -import org.workcraft.workspace.WorkspaceEntry; |
363 | - |
364 | - |
365 | -public class CheckCircuitDeadlockTask extends MpsatChainTask { |
366 | - private final MpsatSettings settings; |
367 | - private final WorkspaceEntry we; |
368 | - private final Framework framework; |
369 | - |
370 | - public CheckCircuitDeadlockTask(WorkspaceEntry we, Framework framework) { |
371 | - super (we, null, framework); |
372 | - this.we = we; |
373 | - this.framework = framework; |
374 | - this.settings = new MpsatSettings("Deadlock freedom", MpsatMode.DEADLOCK, 0, |
375 | - MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), null); |
376 | - } |
377 | - |
378 | - @Override |
379 | - public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
380 | - try { |
381 | - monitor.progressUpdate(0.05); |
382 | - VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel(); |
383 | - STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel(); |
384 | - monitor.progressUpdate(0.10); |
385 | - |
386 | - Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG); |
387 | - if (exporter == null) { |
388 | - throw new RuntimeException ("Exporter not available: model class " + model.getClass().getName() + " to format STG."); |
389 | - } |
390 | - |
391 | - File netFile = File.createTempFile("net", exporter.getExtenstion()); |
392 | - ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
393 | - SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
394 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
395 | - if (exportResult.getOutcome() != Outcome.FINISHED) { |
396 | - netFile.delete(); |
397 | - if (exportResult.getOutcome() == Outcome.CANCELLED) { |
398 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
399 | - } |
400 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
401 | - new MpsatChainResult(exportResult, null, null, settings)); |
402 | - } |
403 | - monitor.progressUpdate(0.20); |
404 | - |
405 | - File mciFile = File.createTempFile("unfolding", ".mci"); |
406 | - PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
407 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
408 | - netFile.delete(); |
409 | - if (punfResult.getOutcome() != Outcome.FINISHED) { |
410 | - mciFile.delete(); |
411 | - if (punfResult.getOutcome() == Outcome.CANCELLED) { |
412 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
413 | - } |
414 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
415 | - new MpsatChainResult(exportResult, punfResult, null, settings)); |
416 | - } |
417 | - monitor.progressUpdate(0.70); |
418 | - |
419 | - MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath()); |
420 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon); |
421 | - if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
422 | - if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
423 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
424 | - } |
425 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
426 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings )); |
427 | - } |
428 | - monitor.progressUpdate(0.90); |
429 | - |
430 | - MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue()); |
431 | - if (!mdp.getSolutions().isEmpty()) { |
432 | - mciFile.delete(); |
433 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
434 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit has a deadlock")); |
435 | - } |
436 | - monitor.progressUpdate(1.0); |
437 | - |
438 | - mciFile.delete(); |
439 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
440 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit is deadlock-free")); |
441 | - |
442 | - } catch (Throwable e) { |
443 | - return new Result<MpsatChainResult>(e); |
444 | - } |
445 | - } |
446 | - |
447 | -} |
448 | |
449 | === removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java' |
450 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java 2014-04-16 21:55:15 +0000 |
451 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java 1970-01-01 00:00:00 +0000 |
452 | @@ -1,110 +0,0 @@ |
453 | -package org.workcraft.plugins.circuit.tasks; |
454 | - |
455 | -import java.io.File; |
456 | - |
457 | -import org.workcraft.Framework; |
458 | -import org.workcraft.interop.Exporter; |
459 | -import org.workcraft.plugins.circuit.VisualCircuit; |
460 | -import org.workcraft.plugins.circuit.tools.STGGenerator; |
461 | -import org.workcraft.plugins.mpsat.MpsatMode; |
462 | -import org.workcraft.plugins.mpsat.MpsatResultParser; |
463 | -import org.workcraft.plugins.mpsat.MpsatSettings; |
464 | -import org.workcraft.plugins.mpsat.MpsatUtilitySettings; |
465 | -import org.workcraft.plugins.mpsat.tasks.MpsatChainResult; |
466 | -import org.workcraft.plugins.mpsat.tasks.MpsatChainTask; |
467 | -import org.workcraft.plugins.mpsat.tasks.MpsatTask; |
468 | -import org.workcraft.plugins.mpsat.tasks.PunfTask; |
469 | -import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
470 | -import org.workcraft.plugins.stg.STGModel; |
471 | -import org.workcraft.serialisation.Format; |
472 | -import org.workcraft.tasks.ProgressMonitor; |
473 | -import org.workcraft.tasks.Result; |
474 | -import org.workcraft.tasks.Result.Outcome; |
475 | -import org.workcraft.tasks.SubtaskMonitor; |
476 | -import org.workcraft.util.Export; |
477 | -import org.workcraft.util.Export.ExportTask; |
478 | -import org.workcraft.workspace.WorkspaceEntry; |
479 | - |
480 | - |
481 | -public class CheckCircuitHazardTask extends MpsatChainTask { |
482 | - private final MpsatSettings settings; |
483 | - private final WorkspaceEntry we; |
484 | - private final Framework framework; |
485 | - |
486 | - public CheckCircuitHazardTask(WorkspaceEntry we, Framework framework) { |
487 | - super (we, null, framework); |
488 | - this.we = we; |
489 | - this.framework = framework; |
490 | - this.settings = new MpsatSettings("Output persistence", MpsatMode.STG_REACHABILITY, 0, |
491 | - MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), |
492 | - MpsatSettings.reachSemimodularity); |
493 | -} |
494 | - |
495 | - @Override |
496 | - public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
497 | - try { |
498 | - monitor.progressUpdate(0.05); |
499 | - VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel(); |
500 | - STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel(); |
501 | - monitor.progressUpdate(0.10); |
502 | - |
503 | - Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG); |
504 | - if (exporter == null) { |
505 | - throw new RuntimeException ("Exporter not available: model class " + model.getClass().getName() + " to format STG."); |
506 | - } |
507 | - |
508 | - File netFile = File.createTempFile("net", exporter.getExtenstion()); |
509 | - ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
510 | - SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
511 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
512 | - if (exportResult.getOutcome() != Outcome.FINISHED) { |
513 | - netFile.delete(); |
514 | - if (exportResult.getOutcome() == Outcome.CANCELLED) { |
515 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
516 | - } |
517 | - return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, settings)); |
518 | - } |
519 | - monitor.progressUpdate(0.20); |
520 | - |
521 | - File mciFile = File.createTempFile("unfolding", ".mci"); |
522 | - PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
523 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
524 | - netFile.delete(); |
525 | - if (punfResult.getOutcome() != Outcome.FINISHED) { |
526 | - mciFile.delete(); |
527 | - if (punfResult.getOutcome() == Outcome.CANCELLED) { |
528 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
529 | - } |
530 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
531 | - new MpsatChainResult(exportResult, punfResult, null, settings)); |
532 | - } |
533 | - monitor.progressUpdate(0.70); |
534 | - |
535 | - MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath()); |
536 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon); |
537 | - if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
538 | - if (mpsatResult.getOutcome() == Outcome.CANCELLED) |
539 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
540 | - |
541 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
542 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings)); |
543 | - } |
544 | - |
545 | - MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue()); |
546 | - if (!mdp.getSolutions().isEmpty()) { |
547 | - mciFile.delete(); |
548 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
549 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit has hazard(s)")); |
550 | - } |
551 | - monitor.progressUpdate(1.0); |
552 | - |
553 | - mciFile.delete(); |
554 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
555 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit is hazard-free")); |
556 | - |
557 | - } catch (Throwable e) { |
558 | - return new Result<MpsatChainResult>(e); |
559 | - } |
560 | - } |
561 | - |
562 | -} |
563 | |
564 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java' |
565 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java 2014-04-16 21:55:15 +0000 |
566 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java 2014-04-29 16:24:51 +0000 |
567 | @@ -14,8 +14,10 @@ |
568 | import org.workcraft.plugins.mpsat.tasks.MpsatChainTask; |
569 | import org.workcraft.plugins.mpsat.tasks.MpsatTask; |
570 | import org.workcraft.plugins.mpsat.tasks.PunfTask; |
571 | +import org.workcraft.plugins.pcomp.PCompOutputMode; |
572 | +import org.workcraft.plugins.pcomp.tasks.PcompTask; |
573 | import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
574 | -import org.workcraft.plugins.stg.STGModel; |
575 | +import org.workcraft.plugins.stg.STG; |
576 | import org.workcraft.serialisation.Format; |
577 | import org.workcraft.tasks.ProgressMonitor; |
578 | import org.workcraft.tasks.Result; |
579 | @@ -23,111 +25,254 @@ |
580 | import org.workcraft.tasks.SubtaskMonitor; |
581 | import org.workcraft.util.Export; |
582 | import org.workcraft.util.Export.ExportTask; |
583 | +import org.workcraft.util.FileUtils; |
584 | import org.workcraft.workspace.WorkspaceEntry; |
585 | |
586 | |
587 | public class CheckCircuitTask extends MpsatChainTask { |
588 | - private final MpsatSettings deadlockSettings; |
589 | - private final MpsatSettings hazardSettings; |
590 | + private final MpsatSettings toolchainPreparationSettings = new MpsatSettings("Toolchain preparation of data", |
591 | + MpsatMode.UNDEFINED, 0, null, 0, null); |
592 | + |
593 | + private final MpsatSettings toolchainCompletionSettings = new MpsatSettings("Toolchain completion", |
594 | + MpsatMode.UNDEFINED, 0, null, 0, null); |
595 | + |
596 | + private final MpsatSettings deadlockSettings = new MpsatSettings("Deadlock freedom", |
597 | + MpsatMode.DEADLOCK, 0, MpsatUtilitySettings.getSolutionMode(), |
598 | + MpsatUtilitySettings.getSolutionCount(), null); |
599 | + |
600 | + private final MpsatSettings hazardSettings = new MpsatSettings("Output persistence", |
601 | + MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), |
602 | + MpsatUtilitySettings.getSolutionCount(), MpsatSettings.reachSemimodularity); |
603 | + |
604 | private final WorkspaceEntry we; |
605 | private final Framework framework; |
606 | + private final boolean checkConformation; |
607 | + private final boolean checkDeadlock; |
608 | + private final boolean checkHazard; |
609 | |
610 | - public CheckCircuitTask(WorkspaceEntry we, Framework framework) { |
611 | + public CheckCircuitTask(WorkspaceEntry we, Framework framework, |
612 | + boolean checkConformation, boolean checkDeadlock, boolean checkHazard) { |
613 | super (we, null, framework); |
614 | this.we = we; |
615 | this.framework = framework; |
616 | - |
617 | - this.deadlockSettings = new MpsatSettings("Deadlock freedom", MpsatMode.DEADLOCK, 0, |
618 | - MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), null); |
619 | - |
620 | - this.hazardSettings = new MpsatSettings("Output persistence", MpsatMode.STG_REACHABILITY, 0, |
621 | - MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), |
622 | - MpsatSettings.reachSemimodularity); |
623 | + this.checkConformation = checkConformation; |
624 | + this.checkDeadlock = checkDeadlock; |
625 | + this.checkHazard = checkHazard; |
626 | } |
627 | |
628 | @Override |
629 | public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
630 | try { |
631 | + // Common variables |
632 | monitor.progressUpdate(0.05); |
633 | - VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel(); |
634 | - STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel(); |
635 | + String title = we.getWorkspacePath().getNode(); |
636 | + if (title.endsWith(".work")) { |
637 | + title = title.substring(0, title.length() - 5); |
638 | + } |
639 | + VisualCircuit visualCircuit = (VisualCircuit)we.getModelEntry().getVisualModel(); |
640 | + STG circuitStg = (STG)STGGenerator.generate(visualCircuit).getMathModel(); |
641 | + Exporter stgExporter = Export.chooseBestExporter(framework.getPluginManager(), circuitStg, Format.STG); |
642 | + if (stgExporter == null) { |
643 | + throw new RuntimeException ("Exporter not available: model class " + circuitStg.getClass().getName() + " to format STG."); |
644 | + } |
645 | + SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor); |
646 | monitor.progressUpdate(0.10); |
647 | - |
648 | - Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG); |
649 | - if (exporter == null) { |
650 | - throw new RuntimeException ("Exporter not available: model class " + model.getClass().getName() + " to format STG."); |
651 | - } |
652 | - |
653 | - File netFile = File.createTempFile("net", exporter.getExtenstion()); |
654 | - ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
655 | - SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
656 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
657 | - if (exportResult.getOutcome() != Outcome.FINISHED) { |
658 | - netFile.delete(); |
659 | - if (exportResult.getOutcome() == Outcome.CANCELLED) { |
660 | + |
661 | + // Generating .g for the circuit |
662 | + File circuitStgFile = File.createTempFile(title + "-circuit-", stgExporter.getExtenstion()); |
663 | + ExportTask circuitExportTask = new ExportTask(stgExporter, circuitStg, circuitStgFile.getCanonicalPath()); |
664 | + Result<? extends Object> circuitExportResult = framework.getTaskManager().execute( |
665 | + circuitExportTask, "Exporting circuit .g", subtaskMonitor); |
666 | + |
667 | + if (circuitExportResult.getOutcome() != Outcome.FINISHED) { |
668 | + circuitStgFile.delete(); |
669 | + if (circuitExportResult.getOutcome() == Outcome.CANCELLED) { |
670 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
671 | } |
672 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
673 | - new MpsatChainResult(exportResult, null, null, deadlockSettings)); |
674 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
675 | + new MpsatChainResult(circuitExportResult, null, null, null, toolchainPreparationSettings)); |
676 | } |
677 | monitor.progressUpdate(0.20); |
678 | |
679 | - File mciFile = File.createTempFile("unfolding", ".mci"); |
680 | - PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
681 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
682 | - netFile.delete(); |
683 | + // Generating .g for the environment |
684 | + File stgFile; |
685 | + STG stg; |
686 | + Result<? extends ExternalProcessResult> pcompResult = null; |
687 | + File environmentFile = visualCircuit.getEnvironmentFile(); |
688 | + boolean hasEnvironment = ((environmentFile != null) && environmentFile.exists()); |
689 | + if ( !hasEnvironment ) { |
690 | + // No environment to compose with |
691 | + stgFile = circuitStgFile; |
692 | + stg = circuitStg; |
693 | + } else { |
694 | + // Compose circuit with its environment |
695 | + File environmentStgFile; |
696 | + if (environmentFile.getName().endsWith(".g")) { |
697 | + environmentStgFile = environmentFile; |
698 | + } else { |
699 | + STG environementStg = (STG)framework.loadFile(environmentFile).getMathModel(); |
700 | + environmentStgFile = File.createTempFile(title + "-environment-", stgExporter.getExtenstion()); |
701 | + ExportTask environmentExportTask = new ExportTask(stgExporter, environementStg, environmentStgFile.getCanonicalPath()); |
702 | + Result<? extends Object> environmentExportResult = framework.getTaskManager().execute( |
703 | + environmentExportTask, "Exporting environment .g", subtaskMonitor); |
704 | + |
705 | + if (environmentExportResult.getOutcome() != Outcome.FINISHED) { |
706 | + environmentStgFile.delete(); |
707 | + if (environmentExportResult.getOutcome() == Outcome.CANCELLED) { |
708 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
709 | + } |
710 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
711 | + new MpsatChainResult(environmentExportResult, null, null, null, toolchainPreparationSettings)); |
712 | + } |
713 | + } |
714 | + monitor.progressUpdate(0.25); |
715 | + |
716 | + // Generating .g for the whole system (circuit and environment) |
717 | + stgFile = File.createTempFile(title + "-system-", stgExporter.getExtenstion()); |
718 | + PcompTask pcompTask = new PcompTask(new File[]{circuitStgFile, environmentStgFile}, PCompOutputMode.OUTPUT, false); |
719 | + pcompResult = framework.getTaskManager().execute( |
720 | + pcompTask, "Running pcomp", subtaskMonitor); |
721 | + |
722 | + if (pcompResult.getOutcome() != Outcome.FINISHED) { |
723 | + circuitStgFile.delete(); |
724 | + if (pcompResult.getOutcome() == Outcome.CANCELLED) { |
725 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
726 | + } |
727 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
728 | + new MpsatChainResult(circuitExportResult, pcompResult, null, null, toolchainPreparationSettings)); |
729 | + } |
730 | + FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput())); |
731 | + WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true); |
732 | + stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel(); |
733 | + } |
734 | + monitor.progressUpdate(0.30); |
735 | + |
736 | + // Generate unfolding |
737 | + File mciFile = File.createTempFile(title+"-unfolding-", ".mci"); |
738 | + PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
739 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
740 | + punfTask, "Unfolding .g", subtaskMonitor); |
741 | + |
742 | + stgFile.delete(); |
743 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
744 | mciFile.delete(); |
745 | if (punfResult.getOutcome() == Outcome.CANCELLED) { |
746 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
747 | } |
748 | return new Result<MpsatChainResult>(Outcome.FAILED, |
749 | - new MpsatChainResult(exportResult, punfResult, null, deadlockSettings)); |
750 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainPreparationSettings)); |
751 | } |
752 | monitor.progressUpdate(0.40); |
753 | - |
754 | - MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
755 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon); |
756 | - if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
757 | - if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
758 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
759 | - } |
760 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
761 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings)); |
762 | + |
763 | + // Check for interface conformation (only if the environment is specified) |
764 | + if (hasEnvironment && checkConformation) { |
765 | + String reachConformation = MpsatSettings.genReachConformation(stg, circuitStg); |
766 | + if (MpsatUtilitySettings.getDebugReach()) { |
767 | + System.out.println("\nReach expression for the interface conformation property:"); |
768 | + System.out.println(reachConformation); |
769 | + } |
770 | + MpsatSettings conformationSettings = new MpsatSettings("Interface conformation", |
771 | + MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), |
772 | + MpsatUtilitySettings.getSolutionCount(), reachConformation); |
773 | + |
774 | + MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
775 | + Result<? extends ExternalProcessResult> mpsatConformationResult = framework.getTaskManager().execute( |
776 | + mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor); |
777 | + |
778 | + if (mpsatConformationResult.getOutcome() != Outcome.FINISHED) { |
779 | + if (mpsatConformationResult.getOutcome() == Outcome.CANCELLED) { |
780 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
781 | + } |
782 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
783 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings)); |
784 | + } |
785 | + monitor.progressUpdate(0.50); |
786 | + |
787 | + MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue()); |
788 | + if (!mpsatConformationParser.getSolutions().isEmpty()) { |
789 | + mciFile.delete(); |
790 | + return new Result<MpsatChainResult>(Outcome.FINISHED, |
791 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, |
792 | + "Circuit does not conform to the environment after the following trace:")); |
793 | + } |
794 | } |
795 | monitor.progressUpdate(0.60); |
796 | |
797 | - MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue()); |
798 | - if (!mdp.getSolutions().isEmpty()) { |
799 | - mciFile.delete(); |
800 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
801 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings, "Circuit has a deadlock")); |
802 | - } |
803 | - monitor.progressUpdate(0.70); |
804 | - |
805 | - mpsatTask = new MpsatTask(hazardSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
806 | - mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon); |
807 | - if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
808 | - if (mpsatResult.getOutcome() == Outcome.CANCELLED) |
809 | - return new Result<MpsatChainResult>(Outcome.CANCELLED); |
810 | - |
811 | - return new Result<MpsatChainResult>(Outcome.FAILED, |
812 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings)); |
813 | - } |
814 | - monitor.progressUpdate(0.90); |
815 | - |
816 | - mdp = new MpsatResultParser(mpsatResult.getReturnValue()); |
817 | - if (!mdp.getSolutions().isEmpty()) { |
818 | - mciFile.delete(); |
819 | - return new Result<MpsatChainResult>(Outcome.FINISHED, |
820 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Circuit has hazard(s)")); |
821 | + // Check for deadlock |
822 | + if (checkDeadlock) { |
823 | + MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
824 | + Result<? extends ExternalProcessResult> mpsatDeadlockResult = framework.getTaskManager().execute( |
825 | + mpsatDeadlockTask, "Running deadlock check [MPSat]", subtaskMonitor); |
826 | + |
827 | + if (mpsatDeadlockResult.getOutcome() != Outcome.FINISHED) { |
828 | + if (mpsatDeadlockResult.getOutcome() == Outcome.CANCELLED) { |
829 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
830 | + } |
831 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
832 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings)); |
833 | + } |
834 | + monitor.progressUpdate(0.70); |
835 | + |
836 | + MpsatResultParser mpsatDeadlockParser = new MpsatResultParser(mpsatDeadlockResult.getReturnValue()); |
837 | + if (!mpsatDeadlockParser.getSolutions().isEmpty()) { |
838 | + mciFile.delete(); |
839 | + return new Result<MpsatChainResult>(Outcome.FINISHED, |
840 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, |
841 | + "Circuit has a deadlock after the following trace:")); |
842 | + } |
843 | + } |
844 | + monitor.progressUpdate(0.80); |
845 | + |
846 | + // Check for hazards |
847 | + if (checkHazard) { |
848 | + MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
849 | + if (MpsatUtilitySettings.getDebugReach()) { |
850 | + System.out.println("\nReach expression for the hazard property:"); |
851 | + System.out.println(hazardSettings.getReach()); |
852 | + } |
853 | + Result<? extends ExternalProcessResult> mpsatHazardResult = framework.getTaskManager().execute( |
854 | + mpsatHazardTask, "Running hazard check [MPSat]", subtaskMonitor); |
855 | + |
856 | + if (mpsatHazardResult.getOutcome() != Outcome.FINISHED) { |
857 | + if (mpsatHazardResult.getOutcome() == Outcome.CANCELLED) { |
858 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
859 | + } |
860 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
861 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings)); |
862 | + } |
863 | + monitor.progressUpdate(0.90); |
864 | + |
865 | + MpsatResultParser mpsatHazardParser = new MpsatResultParser(mpsatHazardResult.getReturnValue()); |
866 | + if (!mpsatHazardParser.getSolutions().isEmpty()) { |
867 | + mciFile.delete(); |
868 | + return new Result<MpsatChainResult>(Outcome.FINISHED, |
869 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, |
870 | + "Circuit has a hazard after the following trace:")); |
871 | + } |
872 | } |
873 | monitor.progressUpdate(1.0); |
874 | |
875 | + // Success |
876 | mciFile.delete(); |
877 | + String message = ""; |
878 | + if (hasEnvironment) { |
879 | + message = "Under the given environment (" + environmentFile.getName() + ")"; |
880 | + } else { |
881 | + message = "Without environment restrictions"; |
882 | + } |
883 | + message += " the circuit is:\n"; |
884 | + if (checkConformation) { |
885 | + message += " * conformant\n"; |
886 | + } |
887 | + if (checkDeadlock) { |
888 | + message += " * deadlock-free\n"; |
889 | + } |
890 | + if (checkHazard) { |
891 | + message += " * hazard-free\n"; |
892 | + } |
893 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
894 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Circuit is deadlock-free and hazard-free")); |
895 | - |
896 | + new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message)); |
897 | + |
898 | } catch (Throwable e) { |
899 | return new Result<MpsatChainResult>(e); |
900 | } |
901 | |
902 | === removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java' |
903 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java 2013-09-17 14:58:15 +0000 |
904 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java 1970-01-01 00:00:00 +0000 |
905 | @@ -1,43 +0,0 @@ |
906 | -package org.workcraft.plugins.circuit.tools; |
907 | - |
908 | -import org.workcraft.Framework; |
909 | -import org.workcraft.Tool; |
910 | -import org.workcraft.plugins.circuit.Circuit; |
911 | -import org.workcraft.plugins.circuit.tasks.CheckCircuitDeadlockTask; |
912 | -import org.workcraft.plugins.mpsat.MpsatChainResultHandler; |
913 | -import org.workcraft.workspace.WorkspaceEntry; |
914 | - |
915 | -public class CheckCircuitDeadlockTool implements Tool { |
916 | - private final Framework framework; |
917 | - |
918 | - public CheckCircuitDeadlockTool(Framework framework) { |
919 | - this.framework = framework; |
920 | - } |
921 | - |
922 | - public String getDisplayName() { |
923 | - return "Check circuit for deadlocks"; |
924 | - } |
925 | - |
926 | - |
927 | - @Override |
928 | - public String getSection() { |
929 | - return "Verification"; |
930 | - } |
931 | - |
932 | - @Override |
933 | - public boolean isApplicableTo(WorkspaceEntry we) { |
934 | - return we.getModelEntry().getMathModel() instanceof Circuit; |
935 | - } |
936 | - |
937 | - @Override |
938 | - public void run(WorkspaceEntry we) { |
939 | - final CheckCircuitDeadlockTask task = new CheckCircuitDeadlockTask(we, framework); |
940 | - String description = "MPSat tool chain"; |
941 | - String title = we.getModelEntry().getModel().getTitle(); |
942 | - if (!title.isEmpty()) { |
943 | - description += "(" + title +")"; |
944 | - } |
945 | - framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task)); |
946 | - } |
947 | - |
948 | -} |
949 | |
950 | === removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java' |
951 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java 2013-09-17 14:58:15 +0000 |
952 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java 1970-01-01 00:00:00 +0000 |
953 | @@ -1,43 +0,0 @@ |
954 | -package org.workcraft.plugins.circuit.tools; |
955 | - |
956 | -import org.workcraft.Framework; |
957 | -import org.workcraft.Tool; |
958 | -import org.workcraft.plugins.circuit.Circuit; |
959 | -import org.workcraft.plugins.circuit.tasks.CheckCircuitHazardTask; |
960 | -import org.workcraft.plugins.mpsat.MpsatChainResultHandler; |
961 | -import org.workcraft.workspace.WorkspaceEntry; |
962 | - |
963 | -public class CheckCircuitHazardTool implements Tool { |
964 | - private final Framework framework; |
965 | - |
966 | - public CheckCircuitHazardTool(Framework framework) { |
967 | - this.framework = framework; |
968 | - } |
969 | - |
970 | - public String getDisplayName() { |
971 | - return "Check circuit for hazards"; |
972 | - } |
973 | - |
974 | - |
975 | - @Override |
976 | - public String getSection() { |
977 | - return "Verification"; |
978 | - } |
979 | - |
980 | - @Override |
981 | - public boolean isApplicableTo(WorkspaceEntry we) { |
982 | - return we.getModelEntry().getMathModel() instanceof Circuit; |
983 | - } |
984 | - |
985 | - @Override |
986 | - public void run(WorkspaceEntry we) { |
987 | - final CheckCircuitHazardTask task = new CheckCircuitHazardTask(we, framework); |
988 | - String description = "MPSat tool chain"; |
989 | - String title = we.getModelEntry().getModel().getTitle(); |
990 | - if (!title.isEmpty()) { |
991 | - description += "(" + title +")"; |
992 | - } |
993 | - framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task)); |
994 | - } |
995 | - |
996 | -} |
997 | |
998 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java' |
999 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java 2013-09-17 14:58:15 +0000 |
1000 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java 2014-04-29 16:24:51 +0000 |
1001 | @@ -15,10 +15,9 @@ |
1002 | } |
1003 | |
1004 | public String getDisplayName() { |
1005 | - return "Check circuit for deadlocks and hazards (reuse unfolding data)"; |
1006 | + return "Check circuit for conformation, deadlocks and hazards (reuse unfolding)"; |
1007 | } |
1008 | |
1009 | - |
1010 | @Override |
1011 | public String getSection() { |
1012 | return "Verification"; |
1013 | @@ -31,7 +30,8 @@ |
1014 | |
1015 | @Override |
1016 | public void run(WorkspaceEntry we) { |
1017 | - final CheckCircuitTask task = new CheckCircuitTask(we, framework); |
1018 | + final CheckCircuitTask task = new CheckCircuitTask(we, framework, |
1019 | + checkConformation(), checkDeadlock(), checkHazard()); |
1020 | String description = "MPSat tool chain"; |
1021 | String title = we.getModelEntry().getModel().getTitle(); |
1022 | if (!title.isEmpty()) { |
1023 | @@ -40,4 +40,16 @@ |
1024 | framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task)); |
1025 | } |
1026 | |
1027 | + public boolean checkConformation() { |
1028 | + return true; |
1029 | + } |
1030 | + |
1031 | + public boolean checkDeadlock() { |
1032 | + return true; |
1033 | + } |
1034 | + |
1035 | + public boolean checkHazard() { |
1036 | + return true; |
1037 | + } |
1038 | + |
1039 | } |
1040 | |
1041 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java' |
1042 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java 2014-01-14 10:38:16 +0000 |
1043 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java 2014-04-29 16:24:51 +0000 |
1044 | @@ -22,6 +22,7 @@ |
1045 | import org.workcraft.dom.visual.VisualNode; |
1046 | import org.workcraft.exceptions.InvalidConnectionException; |
1047 | import org.workcraft.plugins.circuit.Contact; |
1048 | +import org.workcraft.plugins.circuit.Contact.IOType; |
1049 | import org.workcraft.plugins.circuit.VisualCircuit; |
1050 | import org.workcraft.plugins.circuit.VisualCircuitComponent; |
1051 | import org.workcraft.plugins.circuit.VisualCircuitConnection; |
1052 | @@ -29,7 +30,6 @@ |
1053 | import org.workcraft.plugins.circuit.VisualFunctionComponent; |
1054 | import org.workcraft.plugins.circuit.VisualFunctionContact; |
1055 | import org.workcraft.plugins.circuit.VisualJoint; |
1056 | -import org.workcraft.plugins.circuit.Contact.IOType; |
1057 | import org.workcraft.plugins.cpog.optimisation.Literal; |
1058 | import org.workcraft.plugins.cpog.optimisation.booleanvisitors.FormulaToString; |
1059 | import org.workcraft.plugins.cpog.optimisation.dnf.Dnf; |
1060 | @@ -40,9 +40,9 @@ |
1061 | import org.workcraft.plugins.petri.VisualPlace; |
1062 | import org.workcraft.plugins.stg.STG; |
1063 | import org.workcraft.plugins.stg.SignalTransition; |
1064 | +import org.workcraft.plugins.stg.SignalTransition.Direction; |
1065 | import org.workcraft.plugins.stg.VisualSTG; |
1066 | import org.workcraft.plugins.stg.VisualSignalTransition; |
1067 | -import org.workcraft.plugins.stg.SignalTransition.Direction; |
1068 | import org.workcraft.util.Hierarchy; |
1069 | |
1070 | public class STGGenerator { |
1071 | @@ -172,36 +172,34 @@ |
1072 | } |
1073 | |
1074 | // generate implementation for each of the drivers |
1075 | - for(VisualContact c : drivers.keySet()) |
1076 | - { |
1077 | + for(VisualContact c : drivers.keySet()) { |
1078 | if (c instanceof VisualFunctionContact) { |
1079 | // function based driver |
1080 | + Dnf set = null; |
1081 | + Dnf reset = null; |
1082 | VisualFunctionContact contact = (VisualFunctionContact)c; |
1083 | - Dnf set = DnfGenerator.generate(contact.getFunction().getSetFunction()); |
1084 | - Dnf reset = null; |
1085 | - |
1086 | - if (contact.getFunction().getResetFunction()!=null) |
1087 | - reset = DnfGenerator.generate(contact.getFunction().getResetFunction()); |
1088 | - else { |
1089 | - BooleanOperations.worker = new DumbBooleanWorker(); |
1090 | - reset = DnfGenerator.generate(BooleanOperations.worker.not(contact.getFunction().getSetFunction())); |
1091 | - } |
1092 | - |
1093 | SignalTransition.Type ttype = SignalTransition.Type.OUTPUT; |
1094 | - |
1095 | - |
1096 | if (contact.getParent() instanceof VisualCircuitComponent) { |
1097 | - if (((VisualCircuitComponent)contact.getParent()).getIsEnvironment()) |
1098 | - ttype = SignalTransition.Type.INPUT; |
1099 | - else if (contact.getIOType()==IOType.INPUT) |
1100 | + set = DnfGenerator.generate(contact.getFunction().getSetFunction()); |
1101 | + if (contact.getFunction().getResetFunction() != null) { |
1102 | + reset = DnfGenerator.generate(contact.getFunction().getResetFunction()); |
1103 | + } else { |
1104 | + BooleanOperations.worker = new DumbBooleanWorker(); |
1105 | + reset = DnfGenerator.generate(BooleanOperations.worker.not(contact.getFunction().getSetFunction())); |
1106 | + } |
1107 | + if (((VisualCircuitComponent)contact.getParent()).getIsEnvironment()) { |
1108 | + ttype = SignalTransition.Type.INPUT; |
1109 | + } else if (contact.getIOType()==IOType.INPUT) { |
1110 | ttype = SignalTransition.Type.INPUT; |
1111 | + } |
1112 | } else { |
1113 | - if (contact.getIOType()==IOType.INPUT) |
1114 | + set = DnfGenerator.generate(contact.getFunction().getSetFunction()); |
1115 | + reset = DnfGenerator.generate(contact.getFunction().getResetFunction()); |
1116 | + if (contact.getIOType()==IOType.INPUT) { |
1117 | ttype = SignalTransition.Type.INPUT; |
1118 | + } |
1119 | } |
1120 | - |
1121 | implementDriver(circuit, stg, contact, drivers, targetDrivers, set, reset, ttype); |
1122 | - |
1123 | } else { |
1124 | // some generic driver implementation otherwise |
1125 | Dnf set = new Dnf(new DnfClause()); |
1126 | @@ -209,7 +207,6 @@ |
1127 | implementDriver(circuit, stg, c, drivers, targetDrivers, set, reset, SignalTransition.Type.INPUT); |
1128 | } |
1129 | } |
1130 | - |
1131 | return stg; |
1132 | } catch (InvalidConnectionException e) { |
1133 | throw new RuntimeException(e); |
1134 | |
1135 | === modified file 'CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java' |
1136 | --- CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java 2012-07-25 10:32:14 +0000 |
1137 | +++ CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java 2014-04-29 16:24:51 +0000 |
1138 | @@ -20,6 +20,9 @@ |
1139 | public class DnfGenerator { |
1140 | public static Dnf generate(BooleanFormula formula) |
1141 | { |
1142 | + if (formula == null) { |
1143 | + formula = One.instance(); |
1144 | + } |
1145 | return formula.accept(new BooleanVisitor<Dnf>() |
1146 | { |
1147 | boolean negation = false; |
1148 | @@ -218,7 +221,6 @@ |
1149 | |
1150 | } |
1151 | |
1152 | - |
1153 | return simplifyDnf(result); |
1154 | } |
1155 | |
1156 | |
1157 | === modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java' |
1158 | --- DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java 2014-04-08 08:59:38 +0000 |
1159 | +++ DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java 2014-04-29 16:24:51 +0000 |
1160 | @@ -28,7 +28,6 @@ |
1161 | |
1162 | import org.workcraft.annotations.CustomTools; |
1163 | import org.workcraft.annotations.DisplayName; |
1164 | -import org.workcraft.dom.Connection; |
1165 | import org.workcraft.dom.Node; |
1166 | import org.workcraft.dom.math.MathConnection; |
1167 | import org.workcraft.dom.math.MathNode; |
1168 | @@ -221,11 +220,4 @@ |
1169 | return result; |
1170 | } |
1171 | |
1172 | - public Connection getConnection(Node first, Node second) { |
1173 | - for(Connection connection : getConnections(first)) { |
1174 | - if (connection.getSecond() == second) return connection; |
1175 | - } |
1176 | - return null; |
1177 | - } |
1178 | - |
1179 | -} |
1180 | \ No newline at end of file |
1181 | +} |
1182 | |
1183 | === modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java' |
1184 | --- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java 2014-04-16 21:55:15 +0000 |
1185 | +++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java 2014-04-29 16:24:51 +0000 |
1186 | @@ -53,20 +53,24 @@ |
1187 | File netFile = File.createTempFile("net", exporter.getExtenstion()); |
1188 | ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
1189 | SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
1190 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
1191 | + Result<? extends Object> exportResult = framework.getTaskManager().execute( |
1192 | + exportTask, "Exporting .g", mon); |
1193 | + |
1194 | if (exportResult.getOutcome() != Outcome.FINISHED) { |
1195 | netFile.delete(); |
1196 | if (exportResult.getOutcome() == Outcome.CANCELLED) { |
1197 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1198 | } |
1199 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1200 | - new MpsatChainResult(exportResult, null, null, settings)); |
1201 | + new MpsatChainResult(exportResult, null, null, null, settings)); |
1202 | } |
1203 | monitor.progressUpdate(0.20); |
1204 | |
1205 | File mciFile = File.createTempFile("unfolding", ".mci"); |
1206 | PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
1207 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
1208 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
1209 | + punfTask, "Unfolding .g", mon); |
1210 | + |
1211 | netFile.delete(); |
1212 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
1213 | mciFile.delete(); |
1214 | @@ -74,18 +78,21 @@ |
1215 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1216 | } |
1217 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1218 | - new MpsatChainResult(exportResult, punfResult, null, settings)); |
1219 | + new MpsatChainResult(exportResult, null, punfResult, null, settings)); |
1220 | } |
1221 | monitor.progressUpdate(0.70); |
1222 | |
1223 | MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath()); |
1224 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon); |
1225 | + Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute( |
1226 | + mpsatTask, "Running deadlock checking [MPSat]", mon); |
1227 | + |
1228 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
1229 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
1230 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1231 | } |
1232 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1233 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, new String(mpsatResult.getReturnValue().getErrors()))); |
1234 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, |
1235 | + new String(mpsatResult.getReturnValue().getErrors()))); |
1236 | } |
1237 | monitor.progressUpdate(0.90); |
1238 | |
1239 | @@ -93,13 +100,13 @@ |
1240 | if (!mdp.getSolutions().isEmpty()) { |
1241 | mciFile.delete(); |
1242 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1243 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow has a deadlock")); |
1244 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has a deadlock")); |
1245 | } |
1246 | monitor.progressUpdate(1.0); |
1247 | |
1248 | mciFile.delete(); |
1249 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1250 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow is deadlock-free")); |
1251 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is deadlock-free")); |
1252 | |
1253 | } catch (Throwable e) { |
1254 | return new Result<MpsatChainResult>(e); |
1255 | |
1256 | === modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java' |
1257 | --- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java 2014-04-16 21:55:15 +0000 |
1258 | +++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java 2014-04-29 16:24:51 +0000 |
1259 | @@ -54,38 +54,45 @@ |
1260 | File netFile = File.createTempFile("net", exporter.getExtenstion()); |
1261 | ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
1262 | SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
1263 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
1264 | + Result<? extends Object> exportResult = framework.getTaskManager().execute( |
1265 | + exportTask, "Exporting .g", mon); |
1266 | + |
1267 | if (exportResult.getOutcome() != Outcome.FINISHED) { |
1268 | netFile.delete(); |
1269 | if (exportResult.getOutcome() == Outcome.CANCELLED) { |
1270 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1271 | } |
1272 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1273 | - new MpsatChainResult(exportResult, null, null, settings)); |
1274 | + new MpsatChainResult(exportResult, null, null, null, settings)); |
1275 | } |
1276 | monitor.progressUpdate(0.20); |
1277 | |
1278 | File mciFile = File.createTempFile("unfolding", ".mci"); |
1279 | PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
1280 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
1281 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
1282 | + punfTask, "Unfolding .g", mon); |
1283 | + |
1284 | netFile.delete(); |
1285 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
1286 | mciFile.delete(); |
1287 | if (punfResult.getOutcome() == Outcome.CANCELLED) { |
1288 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1289 | } |
1290 | - return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, null, settings)); |
1291 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1292 | + new MpsatChainResult(exportResult, null, punfResult, null, settings)); |
1293 | } |
1294 | monitor.progressUpdate(0.40); |
1295 | |
1296 | MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath()); |
1297 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon); |
1298 | + Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute( |
1299 | + mpsatTask, "Running semimodularity checking [MPSat]", mon); |
1300 | + |
1301 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
1302 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
1303 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1304 | } |
1305 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1306 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings)); |
1307 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings)); |
1308 | } |
1309 | monitor.progressUpdate(0.90); |
1310 | |
1311 | @@ -93,13 +100,13 @@ |
1312 | if (!mdp.getSolutions().isEmpty()) { |
1313 | mciFile.delete(); |
1314 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1315 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow has hazard(s)")); |
1316 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has hazard(s)")); |
1317 | } |
1318 | monitor.progressUpdate(1.0); |
1319 | |
1320 | mciFile.delete(); |
1321 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1322 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow is hazard-free")); |
1323 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is hazard-free")); |
1324 | |
1325 | } catch (Throwable e) { |
1326 | return new Result<MpsatChainResult>(e); |
1327 | |
1328 | === modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java' |
1329 | --- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java 2014-04-16 21:55:15 +0000 |
1330 | +++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java 2014-04-29 16:24:51 +0000 |
1331 | @@ -59,20 +59,24 @@ |
1332 | File netFile = File.createTempFile("net", exporter.getExtenstion()); |
1333 | ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
1334 | SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
1335 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
1336 | + Result<? extends Object> exportResult = framework.getTaskManager().execute( |
1337 | + exportTask, "Exporting .g", mon); |
1338 | + |
1339 | if (exportResult.getOutcome() != Outcome.FINISHED) { |
1340 | netFile.delete(); |
1341 | if (exportResult.getOutcome() == Outcome.CANCELLED) { |
1342 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1343 | } |
1344 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1345 | - new MpsatChainResult(exportResult, null, null, deadlockSettings)); |
1346 | + new MpsatChainResult(exportResult, null, null, null, deadlockSettings)); |
1347 | } |
1348 | monitor.progressUpdate(0.20); |
1349 | |
1350 | File mciFile = File.createTempFile("unfolding", ".mci"); |
1351 | PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
1352 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
1353 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
1354 | + punfTask, "Unfolding .g", mon); |
1355 | + |
1356 | netFile.delete(); |
1357 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
1358 | mciFile.delete(); |
1359 | @@ -80,18 +84,20 @@ |
1360 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1361 | } |
1362 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1363 | - new MpsatChainResult(exportResult, punfResult, null, deadlockSettings)); |
1364 | + new MpsatChainResult(exportResult, null, punfResult, null, deadlockSettings)); |
1365 | } |
1366 | monitor.progressUpdate(0.40); |
1367 | |
1368 | MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath()); |
1369 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon); |
1370 | + Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute( |
1371 | + mpsatTask, "Running deadlock checking [MPSat]", mon); |
1372 | + |
1373 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
1374 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
1375 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1376 | } |
1377 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1378 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings)); |
1379 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, deadlockSettings)); |
1380 | } |
1381 | monitor.progressUpdate(0.60); |
1382 | |
1383 | @@ -99,7 +105,7 @@ |
1384 | if (!mdp.getSolutions().isEmpty()) { |
1385 | mciFile.delete(); |
1386 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1387 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings, "Dataflow has a deadlock")); |
1388 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, deadlockSettings, "Dataflow has a deadlock")); |
1389 | } |
1390 | monitor.progressUpdate(0.70); |
1391 | |
1392 | @@ -110,7 +116,7 @@ |
1393 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1394 | } |
1395 | return new Result<MpsatChainResult>(Outcome.FAILED, |
1396 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings)); |
1397 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings)); |
1398 | } |
1399 | monitor.progressUpdate(0.90); |
1400 | |
1401 | @@ -118,13 +124,13 @@ |
1402 | if (!mdp.getSolutions().isEmpty()) { |
1403 | mciFile.delete(); |
1404 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1405 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Dataflow has hazard(s)")); |
1406 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow has hazard(s)")); |
1407 | } |
1408 | monitor.progressUpdate(1.0); |
1409 | |
1410 | mciFile.delete(); |
1411 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
1412 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Dataflow is deadlock-free and hazard-free")); |
1413 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow is deadlock-free and hazard-free")); |
1414 | |
1415 | } catch (Throwable e) { |
1416 | return new Result<MpsatChainResult>(e); |
1417 | |
1418 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java' |
1419 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java 2014-04-16 21:55:15 +0000 |
1420 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java 2014-04-29 16:24:51 +0000 |
1421 | @@ -26,6 +26,9 @@ |
1422 | if (result.getOutcome() == Outcome.FINISHED) { |
1423 | final MpsatMode mpsatMode = result.getReturnValue().getMpsatSettings().getMode(); |
1424 | switch (mpsatMode) { |
1425 | + case UNDEFINED: |
1426 | + SwingUtilities.invokeLater(new MpsatUndefinedResultHandler(task, result)); |
1427 | + break; |
1428 | case STG_REACHABILITY: |
1429 | case CSC_CONFLICT_DETECTION: |
1430 | case USC_CONFLICT_DETECTION: |
1431 | @@ -41,7 +44,6 @@ |
1432 | case COMPLEX_GATE_IMPLEMENTATION: |
1433 | SwingUtilities.invokeLater(new MpsatSynthesisResultHandler(task, result)); |
1434 | break; |
1435 | - |
1436 | default: |
1437 | SwingUtilities.invokeLater(new Runnable() { |
1438 | @Override |
1439 | @@ -53,57 +55,62 @@ |
1440 | }); |
1441 | break; |
1442 | } |
1443 | - } |
1444 | - else if (result.getOutcome() != Outcome.CANCELLED) { |
1445 | + } else if (result.getOutcome() != Outcome.CANCELLED) { |
1446 | errorMessage = "MPSat tool chain execution failed :-("; |
1447 | - |
1448 | Throwable cause1 = result.getCause(); |
1449 | |
1450 | if (cause1 != null) { |
1451 | // Exception was thrown somewhere in the chain task run() method (not in any of the subtasks) |
1452 | errorMessage += "\n\nFailure caused by: " + cause1.toString() + "\nPlease see the \"Problems\" tab for more details."; |
1453 | - } else |
1454 | - { |
1455 | - Result<? extends Object> exportResult = result.getReturnValue().getExportResult(); |
1456 | - if (exportResult.getOutcome() == Outcome.FAILED) { |
1457 | + } else { |
1458 | + MpsatChainResult returnValue = result.getReturnValue(); |
1459 | + Result<? extends Object> exportResult = returnValue.getExportResult(); |
1460 | + Result<? extends ExternalProcessResult> pcompResult = returnValue.getPcompResult(); |
1461 | + Result<? extends ExternalProcessResult> punfResult = returnValue.getPunfResult(); |
1462 | + Result<? extends ExternalProcessResult> mpsatResult = returnValue.getMpsatResult(); |
1463 | + if (exportResult != null && exportResult.getOutcome() == Outcome.FAILED) { |
1464 | errorMessage += "\n\nFailed to export the model as a .g file."; |
1465 | Throwable cause = exportResult.getCause(); |
1466 | - if (cause != null) |
1467 | - errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details."; |
1468 | - else |
1469 | + if (cause != null) { |
1470 | + errorMessage += "\n\nFailure caused by: " + cause.toString(); |
1471 | + } else { |
1472 | errorMessage += "\n\nThe exporter class did not offer further explanation."; |
1473 | + } |
1474 | + } else if (pcompResult != null && pcompResult.getOutcome() == Outcome.FAILED) { |
1475 | + errorMessage += "\n\nPcomp could not compose the STGs."; |
1476 | + Throwable cause = pcompResult.getCause(); |
1477 | + if (cause != null) { |
1478 | + errorMessage += "\n\nFailure caused by: " + cause.toString(); |
1479 | + } else { |
1480 | + errorMessage += "\n\nFailure caused by the following errors:\n" + new String(pcompResult.getReturnValue().getErrors()); |
1481 | + } |
1482 | + } else if (punfResult != null && punfResult.getOutcome() == Outcome.FAILED) { |
1483 | + errorMessage += "\n\nPunf could not build the unfolding prefix."; |
1484 | + Throwable cause = punfResult.getCause(); |
1485 | + if (cause != null) { |
1486 | + errorMessage += "\n\nFailure caused by: " + cause.toString(); |
1487 | + } else { |
1488 | + errorMessage += "\n\nFailure caused by the following errors:\n" + new String(punfResult.getReturnValue().getErrors()); |
1489 | + } |
1490 | + } else if (mpsatResult != null && mpsatResult.getOutcome() == Outcome.FAILED) { |
1491 | + errorMessage += "\n\nMPSat failed to execute as expected."; |
1492 | + Throwable cause = mpsatResult.getCause(); |
1493 | + if (cause != null) { |
1494 | + errorMessage += "\n\nFailure caused by: " + cause.toString(); |
1495 | + } else { |
1496 | + errorMessage += "\n\nFailure caused by the following errors:\n" + new String(mpsatResult.getReturnValue().getErrors()); |
1497 | + } |
1498 | } else { |
1499 | - Result<? extends ExternalProcessResult> punfResult = result.getReturnValue().getPunfResult(); |
1500 | - |
1501 | - if (punfResult.getOutcome() == Outcome.FAILED) { |
1502 | - errorMessage += "\n\nPunf could not build the unfolding prefix."; |
1503 | - Throwable cause = punfResult.getCause(); |
1504 | - if (cause != null) |
1505 | - errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details."; |
1506 | - else |
1507 | - errorMessage += "\n\nFailure caused by the following errors:\n" + new String(punfResult.getReturnValue().getErrors()); |
1508 | - } else { |
1509 | - Result<? extends ExternalProcessResult> mpsatResult = result.getReturnValue().getMpsatResult(); |
1510 | - |
1511 | - if (mpsatResult.getOutcome() == Outcome.FAILED) { |
1512 | - errorMessage += "\n\nMPSat failed to execute as expected."; |
1513 | - Throwable cause = mpsatResult.getCause(); |
1514 | - if (cause != null) |
1515 | - errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details."; |
1516 | - else |
1517 | - errorMessage += "\n\nFailure caused by the following errors:\n" + new String(mpsatResult.getReturnValue().getErrors()); |
1518 | - } |
1519 | - else { |
1520 | - errorMessage += "\n\nMPSat chain task returned failure status without further explanation. This should not have happened -_-a."; |
1521 | - } |
1522 | - } |
1523 | + errorMessage += "\n\nMPSat chain task returned failure status without further explanation."; |
1524 | } |
1525 | } |
1526 | SwingUtilities.invokeLater(new Runnable() { |
1527 | @Override |
1528 | public void run() { |
1529 | - JOptionPane.showMessageDialog(null, errorMessage, "Oops..", JOptionPane.ERROR_MESSAGE); } |
1530 | + JOptionPane.showMessageDialog(null, errorMessage, "Oops..", JOptionPane.ERROR_MESSAGE); |
1531 | + } |
1532 | }); |
1533 | } |
1534 | } |
1535 | -} |
1536 | \ No newline at end of file |
1537 | + |
1538 | +} |
1539 | |
1540 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java' |
1541 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java 2010-10-06 15:51:01 +0000 |
1542 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java 2014-04-29 16:24:51 +0000 |
1543 | @@ -4,6 +4,7 @@ |
1544 | package org.workcraft.plugins.mpsat; |
1545 | |
1546 | public enum MpsatMode { |
1547 | + UNDEFINED (null, null, false), // Special mode to integrate foreign tasks into Mpsat toolchain (export, composition, unfolding) |
1548 | DEADLOCK ("-D", "Deadlock checking", false), |
1549 | REACHABILITY ("-F", "Reachability analysis", true), |
1550 | STG_REACHABILITY ("-Fs", "STG reachability analysis", true), |
1551 | @@ -20,8 +21,7 @@ |
1552 | private String description; |
1553 | private boolean reach; |
1554 | |
1555 | - public static final MpsatMode[] modes = |
1556 | - { |
1557 | + public static final MpsatMode[] modes = { |
1558 | DEADLOCK, |
1559 | REACHABILITY, |
1560 | STG_REACHABILITY, |
1561 | |
1562 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java' |
1563 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java 2014-04-16 21:55:15 +0000 |
1564 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java 2014-04-29 16:24:51 +0000 |
1565 | @@ -6,9 +6,14 @@ |
1566 | import java.io.File; |
1567 | import java.io.IOException; |
1568 | import java.util.ArrayList; |
1569 | +import java.util.HashSet; |
1570 | import java.util.LinkedHashMap; |
1571 | import java.util.Map; |
1572 | |
1573 | +import org.workcraft.dom.Node; |
1574 | +import org.workcraft.plugins.stg.STG; |
1575 | +import org.workcraft.plugins.stg.SignalTransition; |
1576 | +import org.workcraft.plugins.stg.SignalTransition.Type; |
1577 | import org.workcraft.util.FileUtils; |
1578 | |
1579 | public class MpsatSettings { |
1580 | @@ -33,12 +38,12 @@ |
1581 | } |
1582 | } |
1583 | |
1584 | - private String name = null; |
1585 | - private MpsatMode mode = MpsatMode.DEADLOCK; |
1586 | - private int verbosity = 0; |
1587 | - private SolutionMode solutionMode = SolutionMode.FIRST; |
1588 | - private int solutionNumberLimit = 0; |
1589 | - private String reach = ""; |
1590 | + private final String name; |
1591 | + private final MpsatMode mode; |
1592 | + private final int verbosity; |
1593 | + private final SolutionMode solutionMode; |
1594 | + private final int solutionNumberLimit; |
1595 | + private final String reach; |
1596 | |
1597 | // Reach expression for checking signal consistency |
1598 | public static final String reachConsistency = |
1599 | @@ -52,17 +57,121 @@ |
1600 | |
1601 | // Reach expression for checking semimodularity (output persistency) |
1602 | public static final String reachSemimodularity = |
1603 | - "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n"+ |
1604 | - " exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n"+ |
1605 | - " @t1 &\n"+ |
1606 | - " exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n"+ |
1607 | - " @t2 &\n"+ |
1608 | - " forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n"+ |
1609 | - " exists p in pre t3 \\ post t2 { ~$p }\n"+ |
1610 | - " }\n"+ |
1611 | - " }\n"+ |
1612 | + "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" + |
1613 | + " exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n" + |
1614 | + " @t1 &\n" + |
1615 | + " exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n" + |
1616 | + " @t2 &\n" + |
1617 | + " forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n" + |
1618 | + " exists p in pre t3 \\ post t2 { ~$p }\n" + |
1619 | + " }\n" + |
1620 | + " }\n" + |
1621 | " }\n"; |
1622 | |
1623 | + // Reach expression for checking conformation (this is a template, |
1624 | + // the list of places needs to be updated for each circuit) |
1625 | + public static final String reachConformation = |
1626 | + "let CPnames = {\"in1_0\", \"in1_1\", \"in0_0\", \"in0_1\", \"out0_0\", \"out0_1\"},\n" + |
1627 | + "CP=gather n in CPnames { P n } {\n" + |
1628 | + " exists s in SIGNALS \\ DUMMY {\n" + |
1629 | + " exists t in tran s {\n" + |
1630 | + " forall p in pre t * CP { $p }\n" + |
1631 | + " }\n" + |
1632 | + " &\n" + |
1633 | + " forall t in tran s {\n" + |
1634 | + " exists p in pre t \\ CP { ~$p }\n" + |
1635 | + " }\n" + |
1636 | + " }\n" + |
1637 | + "}\n"; |
1638 | + |
1639 | + // FIXME: Currently Punf does not support dead signals, transitions and places well |
1640 | + // (e.g. a dead transition may disappear from unfolding), therefore the |
1641 | + // conformation property cannot be checked reliably. |
1642 | + public static String genReachConformation(STG stg, STG circuitStg) { |
1643 | + // Form a set of system STG places which came from the circuitStg |
1644 | + HashSet<Node> circuitPlaces = new HashSet<Node>(); |
1645 | + for (Type type: Type.values()) { |
1646 | + for (String s : circuitStg.getSignalNames(type)) { |
1647 | + Node p0 = stg.getNodeByReference(s + "_0"); |
1648 | + if (p0 == null) { |
1649 | + p0 = stg.getNodeByReference("<" + s + "-," + s + "+>"); |
1650 | + } |
1651 | + if (p0 != null) { |
1652 | + circuitPlaces.add(p0); |
1653 | + } |
1654 | + Node p1 = stg.getNodeByReference(s + "_1"); |
1655 | + if (p1 == null) { |
1656 | + p1 = stg.getNodeByReference("<" + s + "+," + s + "->"); |
1657 | + } |
1658 | + if (p1 != null) { |
1659 | + circuitPlaces.add(p1); |
1660 | + } |
1661 | + } |
1662 | + } |
1663 | + // Generate Reach expression |
1664 | + String result = ""; |
1665 | + for (String s : circuitStg.getSignalNames(Type.OUTPUT)) { |
1666 | + String circuitPredicate = ""; |
1667 | + String environmentPredicate = ""; |
1668 | + for (SignalTransition t: stg.getSignalTransitions(Type.OUTPUT)) { |
1669 | + if (!t.getSignalName().equals(s)) continue; |
1670 | + String circuitPreset = ""; |
1671 | + String environmentPreset = ""; |
1672 | + for (Node p: stg.getPreset(t)) { |
1673 | + String name = stg.getNodeReference(p); |
1674 | + if (circuitPlaces.contains(p)) { |
1675 | + if (circuitPreset.isEmpty()) { |
1676 | + circuitPreset += "{"; |
1677 | + } else { |
1678 | + circuitPreset += ", "; |
1679 | + } |
1680 | + circuitPreset += "\"" + name + "\""; |
1681 | + } else { |
1682 | + if (environmentPreset.isEmpty()) { |
1683 | + environmentPreset += "{"; |
1684 | + } else { |
1685 | + environmentPreset += ", "; |
1686 | + } |
1687 | + environmentPreset += "\"" + name + "\""; |
1688 | + } |
1689 | + } |
1690 | + circuitPreset += "}"; |
1691 | + environmentPreset += "}"; |
1692 | + |
1693 | + if (circuitPredicate.isEmpty()) { |
1694 | + circuitPredicate += " (\n"; |
1695 | + } else { |
1696 | + circuitPredicate += " |\n"; |
1697 | + } |
1698 | + circuitPredicate += " forall p in " + circuitPreset + " {\n"; |
1699 | + circuitPredicate += " $ P p\n"; |
1700 | + circuitPredicate += " }\n"; |
1701 | + |
1702 | + if (environmentPredicate.isEmpty()) { |
1703 | + environmentPredicate += " (\n"; |
1704 | + } else { |
1705 | + environmentPredicate += " &\n"; |
1706 | + } |
1707 | + environmentPredicate += " exists p in " + environmentPreset + " {\n"; |
1708 | + environmentPredicate += " ~$ P p\n"; |
1709 | + environmentPredicate += " }\n"; |
1710 | + } |
1711 | + circuitPredicate += " )\n"; |
1712 | + environmentPredicate += " )\n"; |
1713 | + if (!result.isEmpty()) { |
1714 | + result += "|\n"; |
1715 | + } |
1716 | + result += "/* Conformation check for signal " + s + " */\n"; |
1717 | + result += "(\n"; |
1718 | + result += circuitPredicate; |
1719 | + result += " &\n"; |
1720 | + result += environmentPredicate; |
1721 | + result += ")\n"; |
1722 | + } |
1723 | + return result; |
1724 | + } |
1725 | + |
1726 | + |
1727 | public MpsatSettings(String name, MpsatMode mode, int verbosity, SolutionMode solutionMode, int solutionNumberLimit, String reach) { |
1728 | super(); |
1729 | this.name = name; |
1730 | @@ -122,10 +231,11 @@ |
1731 | break; |
1732 | case ALL: |
1733 | int solutionNumberLimit = getSolutionNumberLimit(); |
1734 | - if (solutionNumberLimit>0) |
1735 | + if (solutionNumberLimit>0) { |
1736 | args.add("-a" + Integer.toString(solutionNumberLimit)); |
1737 | - else |
1738 | + } else { |
1739 | args.add("-a"); |
1740 | + } |
1741 | } |
1742 | |
1743 | return args.toArray(new String[args.size()]); |
1744 | |
1745 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java' |
1746 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java 2014-04-16 21:55:15 +0000 |
1747 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java 2014-04-29 16:24:51 +0000 |
1748 | @@ -22,24 +22,32 @@ |
1749 | this.result = result; |
1750 | } |
1751 | |
1752 | + private String getPropertyName() { |
1753 | + String propertyName; |
1754 | + MpsatSettings settings = task.getSettings(); |
1755 | + if (settings != null && settings.getName() != null) { |
1756 | + propertyName = settings.getName(); |
1757 | + } else { |
1758 | + propertyName = "The property"; |
1759 | + } |
1760 | + return propertyName; |
1761 | + } |
1762 | |
1763 | @Override |
1764 | public void run() { |
1765 | MpsatResultParser mdp = new MpsatResultParser(result.getReturnValue().getMpsatResult().getReturnValue()); |
1766 | List<Trace> solutions = mdp.getSolutions(); |
1767 | - String propertyName = task.getSettings().getName(); |
1768 | - if (propertyName == null) { |
1769 | - propertyName = "The property"; |
1770 | - } |
1771 | + String message = result.getReturnValue().getMessage(); |
1772 | if (!solutions.isEmpty()) { |
1773 | - String message = propertyName + " is violated with the following trace:\n"; |
1774 | + if (message == null) { |
1775 | + message = getPropertyName() + " is violated with the following trace:\n"; |
1776 | + } |
1777 | final SolutionsDialog solutionsDialog = new SolutionsDialog(task, message, solutions); |
1778 | GUI.centerAndSizeToParent(solutionsDialog, task.getFramework().getMainWindow()); |
1779 | solutionsDialog.setVisible(true); |
1780 | } else { |
1781 | - String message = result.getReturnValue().getMessage(); |
1782 | if (message == null) { |
1783 | - message = propertyName + " is satisfied."; |
1784 | + message = getPropertyName() + " is satisfied."; |
1785 | } |
1786 | JOptionPane.showMessageDialog(null, message); |
1787 | } |
1788 | |
1789 | === added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java' |
1790 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java 1970-01-01 00:00:00 +0000 |
1791 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java 2014-04-29 16:24:51 +0000 |
1792 | @@ -0,0 +1,32 @@ |
1793 | +package org.workcraft.plugins.mpsat; |
1794 | + |
1795 | +import javax.swing.JOptionPane; |
1796 | + |
1797 | +import org.workcraft.plugins.mpsat.tasks.MpsatChainResult; |
1798 | +import org.workcraft.plugins.mpsat.tasks.MpsatChainTask; |
1799 | +import org.workcraft.tasks.Result; |
1800 | + |
1801 | + |
1802 | +final class MpsatUndefinedResultHandler implements Runnable { |
1803 | + |
1804 | + private final Result<? extends MpsatChainResult> result; |
1805 | + private final MpsatChainTask task; |
1806 | + |
1807 | + MpsatUndefinedResultHandler(MpsatChainTask task, Result<? extends MpsatChainResult> result) { |
1808 | + this.task = task; |
1809 | + this.result = result; |
1810 | + } |
1811 | + |
1812 | + @Override |
1813 | + public void run() { |
1814 | + String message = result.getReturnValue().getMessage(); |
1815 | + if (message == null) { |
1816 | + MpsatSettings settings = task.getSettings(); |
1817 | + if (settings != null && settings.getName() != null) { |
1818 | + message = settings.getName(); |
1819 | + } |
1820 | + } |
1821 | + JOptionPane.showMessageDialog(null, message); |
1822 | + } |
1823 | + |
1824 | +} |
1825 | |
1826 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java' |
1827 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java 2013-10-15 12:25:49 +0000 |
1828 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java 2014-04-29 16:24:51 +0000 |
1829 | @@ -35,10 +35,12 @@ |
1830 | private static final String commandKey = "Tools.mpsat.command"; |
1831 | private static final String solutionModeKey = "Tools.mpsat.solutionMode"; |
1832 | private static final String extraArgsKey = "Tools.mpsat.args"; |
1833 | + private static final String debugReachKey = "Tools.mpsat.debugReach"; |
1834 | |
1835 | private static String command = "mpsat"; |
1836 | private static SolutionMode solutionMode = SolutionMode.MINIMUM_COST; |
1837 | private static String extraArgs = ""; |
1838 | + private static Boolean debugReach = false; |
1839 | |
1840 | public MpsatUtilitySettings() { |
1841 | properties = new LinkedList<PropertyDescriptor>(); |
1842 | @@ -72,6 +74,16 @@ |
1843 | return MpsatUtilitySettings.getExtraArgs(); |
1844 | } |
1845 | }); |
1846 | + |
1847 | + properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>( |
1848 | + this, "MPSat debug", Boolean.class) { |
1849 | + protected void setter(MpsatUtilitySettings object, Boolean value) { |
1850 | + MpsatUtilitySettings.setDebugReach(value); |
1851 | + } |
1852 | + protected Boolean getter(MpsatUtilitySettings object) { |
1853 | + return MpsatUtilitySettings.getDebugReach(); |
1854 | + } |
1855 | + }); |
1856 | } |
1857 | |
1858 | @Override |
1859 | @@ -84,6 +96,7 @@ |
1860 | command = config.getString(commandKey, "mpsat"); |
1861 | solutionMode = config.getEnum(solutionModeKey, SolutionMode.class, SolutionMode.FIRST); |
1862 | extraArgs = config.getString(extraArgsKey, ""); |
1863 | + debugReach = config.getBoolean(debugReachKey, false); |
1864 | } |
1865 | |
1866 | @Override |
1867 | @@ -91,6 +104,7 @@ |
1868 | config.set(commandKey, command); |
1869 | config.setEnum(solutionModeKey, SolutionMode.class, solutionMode); |
1870 | config.set(extraArgsKey, extraArgs); |
1871 | + config.setBoolean(debugReachKey, debugReach); |
1872 | } |
1873 | |
1874 | @Override |
1875 | @@ -130,4 +144,12 @@ |
1876 | public static int getSolutionCount() { |
1877 | return (MpsatUtilitySettings.solutionMode == SolutionMode.ALL) ? 10 : 1; |
1878 | } |
1879 | + |
1880 | + public static Boolean getDebugReach() { |
1881 | + return debugReach; |
1882 | + } |
1883 | + |
1884 | + public static void setDebugReach(Boolean debug) { |
1885 | + MpsatUtilitySettings.debugReach = debug; |
1886 | + } |
1887 | } |
1888 | \ No newline at end of file |
1889 | |
1890 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java' |
1891 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java 2014-04-16 22:13:32 +0000 |
1892 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java 2014-04-29 16:24:51 +0000 |
1893 | @@ -154,7 +154,7 @@ |
1894 | } |
1895 | |
1896 | private void createSolutionModeButtons() { |
1897 | - firstSolutionButton = new JRadioButton ("Find any solution (default)"); |
1898 | + firstSolutionButton = new JRadioButton ("Find any solution"); |
1899 | firstSolutionButton.setSelected(true); |
1900 | firstSolutionButton.addActionListener(new ActionListener() { |
1901 | @Override |
1902 | |
1903 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java' |
1904 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java 2014-04-16 21:55:15 +0000 |
1905 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java 2014-04-29 16:24:51 +0000 |
1906 | @@ -43,7 +43,7 @@ |
1907 | |
1908 | JButton saveButton = new JButton("Save"); |
1909 | |
1910 | - JButton playButton = new JButton("Play trace"); |
1911 | + JButton playButton = new JButton("Play"); |
1912 | playButton.addActionListener(new ActionListener() |
1913 | { |
1914 | @Override |
1915 | |
1916 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java' |
1917 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java 2010-11-18 02:08:34 +0000 |
1918 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java 2014-04-29 16:24:51 +0000 |
1919 | @@ -5,38 +5,47 @@ |
1920 | import org.workcraft.tasks.Result; |
1921 | |
1922 | public class MpsatChainResult { |
1923 | + private Result<? extends Object> exportResult; |
1924 | + private Result<? extends ExternalProcessResult> pcompResult; |
1925 | private Result<? extends ExternalProcessResult> punfResult; |
1926 | private Result<? extends ExternalProcessResult> mpsatResult; |
1927 | - private Result<? extends Object> exportResult; |
1928 | private MpsatSettings mpsatSettings; |
1929 | private String message; |
1930 | + |
1931 | + public MpsatChainResult(Result<? extends Object> exportResult, |
1932 | + Result<? extends ExternalProcessResult> pcompResult, |
1933 | + Result<? extends ExternalProcessResult> punfResult, |
1934 | + Result<? extends ExternalProcessResult> mpsatResult, |
1935 | + MpsatSettings mpsatSettings, String message) { |
1936 | |
1937 | + this.exportResult = exportResult; |
1938 | + this.pcompResult = pcompResult; |
1939 | + this.punfResult = punfResult; |
1940 | + this.mpsatResult = mpsatResult; |
1941 | + this.mpsatSettings = mpsatSettings; |
1942 | + this.message = message; |
1943 | + } |
1944 | + |
1945 | public MpsatChainResult(Result<? extends Object> exportResult, |
1946 | - Result<? extends ExternalProcessResult> punfResult, |
1947 | + Result<? extends ExternalProcessResult> pcompResult, |
1948 | + Result<? extends ExternalProcessResult> punfResult, |
1949 | Result<? extends ExternalProcessResult> mpsatResult, |
1950 | MpsatSettings mpsatSettings) { |
1951 | - this.punfResult = punfResult; |
1952 | - this.mpsatResult = mpsatResult; |
1953 | - this.exportResult = exportResult; |
1954 | - this.mpsatSettings = mpsatSettings; |
1955 | - } |
1956 | - |
1957 | - public MpsatChainResult(Result<? extends Object> exportResult, |
1958 | - Result<? extends ExternalProcessResult> punfResult, |
1959 | - Result<? extends ExternalProcessResult> mpsatResult, |
1960 | - MpsatSettings mpsatSettings, String message) { |
1961 | - |
1962 | - this.punfResult = punfResult; |
1963 | - this.mpsatResult = mpsatResult; |
1964 | - this.exportResult = exportResult; |
1965 | - this.mpsatSettings = mpsatSettings; |
1966 | - |
1967 | - this.message = message; |
1968 | + |
1969 | + this(exportResult, pcompResult, punfResult, mpsatResult, mpsatSettings, null); |
1970 | } |
1971 | |
1972 | public MpsatSettings getMpsatSettings() { |
1973 | return mpsatSettings; |
1974 | } |
1975 | + |
1976 | + public Result<? extends Object> getExportResult() { |
1977 | + return exportResult; |
1978 | + } |
1979 | + |
1980 | + public Result<? extends ExternalProcessResult> getPcompResult() { |
1981 | + return pcompResult; |
1982 | + } |
1983 | |
1984 | public Result<? extends ExternalProcessResult> getPunfResult() { |
1985 | return punfResult; |
1986 | @@ -49,8 +58,4 @@ |
1987 | public String getMessage() { |
1988 | return message; |
1989 | } |
1990 | - |
1991 | - public Result<? extends Object> getExportResult() { |
1992 | - return exportResult; |
1993 | - } |
1994 | } |
1995 | \ No newline at end of file |
1996 | |
1997 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java' |
1998 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java 2014-04-16 21:55:15 +0000 |
1999 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java 2014-04-29 16:24:51 +0000 |
2000 | @@ -50,7 +50,7 @@ |
2001 | netFile.delete(); |
2002 | if (exportResult.getOutcome() == Outcome.CANCELLED) |
2003 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2004 | - return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, settings)); |
2005 | + return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, null, settings)); |
2006 | } |
2007 | monitor.progressUpdate(0.33); |
2008 | |
2009 | @@ -63,7 +63,7 @@ |
2010 | mciFile.delete(); |
2011 | if (punfResult.getOutcome() == Outcome.CANCELLED) |
2012 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2013 | - return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, null, settings)); |
2014 | + return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, punfResult, null, settings)); |
2015 | } |
2016 | |
2017 | monitor.progressUpdate(0.66); |
2018 | @@ -75,12 +75,12 @@ |
2019 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
2020 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) |
2021 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2022 | - return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, mpsatResult, settings )); |
2023 | + return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings )); |
2024 | } |
2025 | |
2026 | monitor.progressUpdate(1.0); |
2027 | |
2028 | - return new Result<MpsatChainResult>(Outcome.FINISHED, new MpsatChainResult(exportResult, punfResult, mpsatResult, settings)); |
2029 | + return new Result<MpsatChainResult>(Outcome.FINISHED, new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings)); |
2030 | } catch (Throwable e) { |
2031 | return new Result<MpsatChainResult>(e); |
2032 | } |
2033 | |
2034 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java' |
2035 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java 2010-09-21 15:39:20 +0000 |
2036 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java 2014-04-29 16:24:51 +0000 |
2037 | @@ -40,9 +40,9 @@ |
2038 | if (result.getCause() != null) { |
2039 | message = result.getCause().getMessage(); |
2040 | result.getCause().printStackTrace(); |
2041 | - } |
2042 | - else |
2043 | + } else { |
2044 | message = "Pcomp errors: \n" + new String(result.getReturnValue().getErrors()); |
2045 | + } |
2046 | JOptionPane.showMessageDialog(framework.getMainWindow(), message, "Parallel composition failed", JOptionPane.ERROR_MESSAGE); |
2047 | } else if (result.getOutcome() == Outcome.FINISHED) { |
2048 | try { |
2049 | |
2050 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java' |
2051 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java 2014-04-16 17:52:01 +0000 |
2052 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java 2014-04-29 16:24:51 +0000 |
2053 | @@ -45,7 +45,9 @@ |
2054 | inputs.add(dotGProvider.getDotG(p)); |
2055 | } |
2056 | |
2057 | - framework.getTaskManager().queue(new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), dialog.isImprovedPcompChecked()), "Running pcomp", new PcompResultHandler(framework, dialog.showInEditor())); |
2058 | + PcompTask pcompTask = new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), dialog.isImprovedPcompChecked()); |
2059 | + PcompResultHandler pcompResult = new PcompResultHandler(framework, dialog.showInEditor()); |
2060 | + framework.getTaskManager().queue(pcompTask, "Running pcomp", pcompResult); |
2061 | } |
2062 | } |
2063 | |
2064 | |
2065 | === modified file 'PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java' |
2066 | --- PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java 2014-04-16 21:55:15 +0000 |
2067 | +++ PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java 2014-04-29 16:24:51 +0000 |
2068 | @@ -53,20 +53,24 @@ |
2069 | File netFile = File.createTempFile("net", exporter.getExtenstion()); |
2070 | ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
2071 | SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
2072 | - Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
2073 | + Result<? extends Object> exportResult = framework.getTaskManager().execute( |
2074 | + exportTask, "Exporting .g", mon); |
2075 | + |
2076 | if (exportResult.getOutcome() != Outcome.FINISHED) { |
2077 | netFile.delete(); |
2078 | if (exportResult.getOutcome() == Outcome.CANCELLED) { |
2079 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2080 | } |
2081 | return new Result<MpsatChainResult>(Outcome.FAILED, |
2082 | - new MpsatChainResult(exportResult, null, null, settings)); |
2083 | + new MpsatChainResult(exportResult, null, null, null, settings)); |
2084 | } |
2085 | monitor.progressUpdate(0.20); |
2086 | |
2087 | File mciFile = File.createTempFile("unfolding", ".mci"); |
2088 | PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath()); |
2089 | - Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
2090 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
2091 | + punfTask, "Unfolding .g", mon); |
2092 | + |
2093 | netFile.delete(); |
2094 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
2095 | mciFile.delete(); |
2096 | @@ -74,18 +78,21 @@ |
2097 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2098 | } |
2099 | return new Result<MpsatChainResult>(Outcome.FAILED, |
2100 | - new MpsatChainResult(exportResult, punfResult, null, settings)); |
2101 | + new MpsatChainResult(exportResult, null, punfResult, null, settings)); |
2102 | } |
2103 | monitor.progressUpdate(0.70); |
2104 | |
2105 | MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath()); |
2106 | - Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon); |
2107 | + Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute( |
2108 | + mpsatTask, "Running deadlock checking [MPSat]", mon); |
2109 | + |
2110 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
2111 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
2112 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
2113 | } |
2114 | return new Result<MpsatChainResult>(Outcome.FAILED, |
2115 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, new String(mpsatResult.getReturnValue().getErrors()))); |
2116 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, |
2117 | + new String(mpsatResult.getReturnValue().getErrors()))); |
2118 | } |
2119 | monitor.progressUpdate(0.90); |
2120 | |
2121 | @@ -93,13 +100,13 @@ |
2122 | if (!mdp.getSolutions().isEmpty()) { |
2123 | mciFile.delete(); |
2124 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
2125 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net has a deadlock")); |
2126 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net has a deadlock")); |
2127 | } |
2128 | monitor.progressUpdate(1.0); |
2129 | |
2130 | mciFile.delete(); |
2131 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
2132 | - new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net is deadlock-free")); |
2133 | + new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net is deadlock-free")); |
2134 | |
2135 | } catch (Throwable e) { |
2136 | return new Result<MpsatChainResult>(e); |
2137 | |
2138 | === modified file 'STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java' |
2139 | --- STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java 2014-04-03 17:30:41 +0000 |
2140 | +++ STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java 2014-04-29 16:24:51 +0000 |
2141 | @@ -20,7 +20,7 @@ |
2142 | |
2143 | public static Pair<String, String> parseImplicitPlaceReference(String ref) { |
2144 | String[] parts = ref.replaceAll(" ", "").split(","); |
2145 | - if (parts.length < 2 || !parts[0].startsWith("<") || !parts[0].endsWith(">")) { |
2146 | + if (parts.length < 2 || !parts[0].startsWith("<") || !parts[1].endsWith(">")) { |
2147 | return null; |
2148 | } |
2149 | return Pair.of(parts[0].substring(1), parts[1].substring(0, parts[1].length()-1)); |
2150 | |
2151 | === modified file 'STGPlugin/src/org/workcraft/plugins/stg/STG.java' |
2152 | --- STGPlugin/src/org/workcraft/plugins/stg/STG.java 2014-04-22 13:51:18 +0000 |
2153 | +++ STGPlugin/src/org/workcraft/plugins/stg/STG.java 2014-04-29 16:24:51 +0000 |
2154 | @@ -320,12 +320,8 @@ |
2155 | throw new RuntimeException( |
2156 | "An implicit place cannot have more that one transition in its preset or postset."); |
2157 | } |
2158 | - return "<" |
2159 | - + referenceManager.getNodeReference(preset.iterator() |
2160 | - .next()) |
2161 | - + "," |
2162 | - + referenceManager.getNodeReference(postset.iterator() |
2163 | - .next()) + ">"; |
2164 | + return "<" + referenceManager.getNodeReference(preset.iterator().next()) + "," |
2165 | + + referenceManager.getNodeReference(postset.iterator().next()) + ">"; |
2166 | } else { |
2167 | return referenceManager.getNodeReference(node); |
2168 | } |
2169 | @@ -335,8 +331,7 @@ |
2170 | } |
2171 | |
2172 | public Node getNodeByReference(String reference) { |
2173 | - Pair<String, String> implicitPlaceTransitions = LabelParser |
2174 | - .parseImplicitPlaceReference(reference); |
2175 | + Pair<String, String> implicitPlaceTransitions = LabelParser.parseImplicitPlaceReference(reference); |
2176 | if (implicitPlaceTransitions != null) { |
2177 | Node t1 = referenceManager |
2178 | .getNodeByReference(implicitPlaceTransitions.getFirst()); |
2179 | |
2180 | === modified file 'STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java' |
2181 | --- STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java 2014-04-17 15:33:40 +0000 |
2182 | +++ STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java 2014-04-29 16:24:51 +0000 |
2183 | @@ -246,12 +246,5 @@ |
2184 | } |
2185 | return null; |
2186 | } |
2187 | - |
2188 | - public Connection getConnection(Node first, Node second) { |
2189 | - for(Connection connection : getConnections(first)) { |
2190 | - if (connection.getSecond() == second) return connection; |
2191 | - } |
2192 | - return null; |
2193 | - } |
2194 | |
2195 | } |
2196 | |
2197 | === modified file 'WorkcraftCore/src/org/workcraft/dom/AbstractModel.java' |
2198 | --- WorkcraftCore/src/org/workcraft/dom/AbstractModel.java 2014-01-29 19:00:22 +0000 |
2199 | +++ WorkcraftCore/src/org/workcraft/dom/AbstractModel.java 2014-04-29 16:24:51 +0000 |
2200 | @@ -131,4 +131,12 @@ |
2201 | protected ReferenceManager getReferenceManager() { |
2202 | return referenceManager; |
2203 | } |
2204 | -} |
2205 | \ No newline at end of file |
2206 | + |
2207 | + public Connection getConnection(Node first, Node second) { |
2208 | + for(Connection connection : getConnections(first)) { |
2209 | + if (connection.getSecond() == second) return connection; |
2210 | + } |
2211 | + return null; |
2212 | + } |
2213 | + |
2214 | +} |
2215 | |
2216 | === modified file 'WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java' |
2217 | --- WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java 2014-04-09 22:33:19 +0000 |
2218 | +++ WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java 2014-04-29 16:24:51 +0000 |
2219 | @@ -11,8 +11,6 @@ |
2220 | import javax.swing.JTable; |
2221 | import javax.swing.table.TableCellEditor; |
2222 | |
2223 | -import org.workcraft.gui.FileFilters; |
2224 | - |
2225 | @SuppressWarnings("serial") |
2226 | public class FileCellEditor extends AbstractCellEditor implements TableCellEditor, ActionListener { |
2227 | |
2228 | @@ -34,7 +32,6 @@ |
2229 | if (EDIT.equals(e.getActionCommand())) { |
2230 | JFileChooser fc = new JFileChooser(); |
2231 | fc.setDialogType(JFileChooser.OPEN_DIALOG); |
2232 | - fc.setFileFilter(FileFilters.DOCUMENT_FILES); |
2233 | fc.setMultiSelectionEnabled(false); |
2234 | fc.setSelectedFile(file); |
2235 | fc.setDialogTitle("Open environment file"); |
2236 | |
2237 | === modified file 'WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java' |
2238 | --- WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java 2012-05-22 09:39:39 +0000 |
2239 | +++ WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java 2014-04-29 16:24:51 +0000 |
2240 | @@ -20,6 +20,8 @@ |
2241 | import org.workcraft.plugins.serialisation.xml.DoubleSerialiser; |
2242 | import org.workcraft.plugins.serialisation.xml.EnumDeserialiser; |
2243 | import org.workcraft.plugins.serialisation.xml.EnumSerialiser; |
2244 | +import org.workcraft.plugins.serialisation.xml.FileDeserialiser; |
2245 | +import org.workcraft.plugins.serialisation.xml.FileSerialiser; |
2246 | import org.workcraft.plugins.serialisation.xml.IntDeserialiser; |
2247 | import org.workcraft.plugins.serialisation.xml.IntSerialiser; |
2248 | import org.workcraft.plugins.serialisation.xml.StringDeserialiser; |
2249 | @@ -46,6 +48,7 @@ |
2250 | p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, BezierSerialiser.class); |
2251 | p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, ConnectionSerialiser.class); |
2252 | p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, VisualConnectionSerialiser.class); |
2253 | + p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, FileSerialiser.class); |
2254 | |
2255 | p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, AffineTransformDeserialiser.class); |
2256 | p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, BooleanDeserialiser.class); |
2257 | @@ -57,6 +60,7 @@ |
2258 | p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, BezierDeserialiser.class); |
2259 | p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, ConnectionDeserialiser.class); |
2260 | p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, VisualConnectionDeserialiser.class); |
2261 | + p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, FileDeserialiser.class); |
2262 | } |
2263 | |
2264 | @Override |
2265 | |
2266 | === added file 'WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java' |
2267 | --- WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java 1970-01-01 00:00:00 +0000 |
2268 | +++ WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java 2014-04-29 16:24:51 +0000 |
2269 | @@ -0,0 +1,19 @@ |
2270 | +package org.workcraft.plugins.serialisation.xml; |
2271 | + |
2272 | +import java.io.File; |
2273 | + |
2274 | +import org.w3c.dom.Element; |
2275 | +import org.workcraft.exceptions.DeserialisationException; |
2276 | +import org.workcraft.serialisation.xml.BasicXMLDeserialiser; |
2277 | + |
2278 | +public class FileDeserialiser implements BasicXMLDeserialiser{ |
2279 | + |
2280 | + public String getClassName() { |
2281 | + return File.class.getName(); |
2282 | + } |
2283 | + |
2284 | + public Object deserialise(Element element) throws DeserialisationException { |
2285 | + return new File(element.getAttribute("path")); |
2286 | + } |
2287 | + |
2288 | +} |
2289 | |
2290 | === added file 'WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java' |
2291 | --- WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java 1970-01-01 00:00:00 +0000 |
2292 | +++ WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java 2014-04-29 16:24:51 +0000 |
2293 | @@ -0,0 +1,22 @@ |
2294 | +package org.workcraft.plugins.serialisation.xml; |
2295 | + |
2296 | +import java.io.File; |
2297 | + |
2298 | +import org.w3c.dom.Element; |
2299 | +import org.workcraft.exceptions.SerialisationException; |
2300 | +import org.workcraft.serialisation.xml.BasicXMLSerialiser; |
2301 | + |
2302 | +public class FileSerialiser implements BasicXMLSerialiser { |
2303 | + |
2304 | + public String getClassName() { |
2305 | + return File.class.getName(); |
2306 | + } |
2307 | + |
2308 | + public void serialise(Element element, Object object) |
2309 | + throws SerialisationException { |
2310 | + if (object != null) { |
2311 | + element.setAttribute("path", ((File)object).getPath()); |
2312 | + } |
2313 | + } |
2314 | + |
2315 | +} |
2316 | |
2317 | === modified file 'WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java' |
2318 | --- WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java 2014-03-13 15:09:13 +0000 |
2319 | +++ WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java 2014-04-29 16:24:51 +0000 |
2320 | @@ -31,12 +31,17 @@ |
2321 | |
2322 | public class CommonEditorSettings implements SettingsPage { |
2323 | private static LinkedList<PropertyDescriptor> properties; |
2324 | - |
2325 | + |
2326 | + private static final String backgroundColorKey = "CommonEditorSettings.backgroundColor"; |
2327 | + private static final String showGridKey = "CommonEditorSettings.showGrid"; |
2328 | + private static final String showRulersKey = "CommonEditorSettings.showRulers"; |
2329 | + private static final String iconSizeKey = "CommonEditorSettings.iconSize"; |
2330 | + private static final String debugClipboardKey = "CommonEditorSettings.debugClipboard"; |
2331 | + |
2332 | protected static Color backgroundColor = Color.WHITE; |
2333 | private static boolean showGrid = true; |
2334 | private static boolean showRulers = true; |
2335 | protected static int iconSize = 24; |
2336 | - |
2337 | private static boolean debugClipboard = false; |
2338 | |
2339 | public String getSection() { |
2340 | @@ -115,19 +120,19 @@ |
2341 | } |
2342 | |
2343 | public void load(Config config) { |
2344 | - backgroundColor = config.getColor("CommonEditorSettings.backgroundColor", Color.WHITE); |
2345 | - showGrid = config.getBoolean("CommonEditorSettings.showGrid", true); |
2346 | - showRulers = config.getBoolean("CommonEditorSettings.showRullers", true); |
2347 | - iconSize = config.getInt("CommonEditorSettings.iconSize", 24); |
2348 | - debugClipboard = config.getBoolean("CommonEditorSettings.debugClipboard", false); |
2349 | + backgroundColor = config.getColor(backgroundColorKey, Color.WHITE); |
2350 | + showGrid = config.getBoolean(showGridKey, true); |
2351 | + showRulers = config.getBoolean(showRulersKey, true); |
2352 | + iconSize = config.getInt(iconSizeKey, 24); |
2353 | + debugClipboard = config.getBoolean(debugClipboardKey, false); |
2354 | } |
2355 | |
2356 | public void save(Config config) { |
2357 | - config.setColor("CommonEditorSettings.backgroundColor", backgroundColor); |
2358 | - config.setBoolean("CommonEditorSettings.showGrid", showGrid); |
2359 | - config.setBoolean("CommonEditorSettings.showRullers", showRulers); |
2360 | - config.setInt("CommonEditorSettings.iconSize", iconSize); |
2361 | - config.setBoolean("CommonEditorSettings.debugClipboard", debugClipboard); |
2362 | + config.setColor(backgroundColorKey, backgroundColor); |
2363 | + config.setBoolean(showGridKey, showGrid); |
2364 | + config.setBoolean(showRulersKey, showRulers); |
2365 | + config.setInt(iconSizeKey, iconSize); |
2366 | + config.setBoolean(debugClipboardKey, debugClipboard); |
2367 | } |
2368 | |
2369 | public static Color getBackgroundColor() { |