Merge lp:~danilovesky/workcraft/trunk-stg-conformation into lp:workcraft
- trunk-stg-conformation
- Merge into trunk
Proposed by
Danil Sokolov
Status: | Merged |
---|---|
Merged at revision: | 572 |
Proposed branch: | lp:~danilovesky/workcraft/trunk-stg-conformation |
Merge into: | lp:workcraft |
Diff against target: |
1804 lines (+711/-334) 26 files modified
CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java (+111/-76) CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java (+2/-2) CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java (+1/-1) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java (+3/-4) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java (+4/-3) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java (+132/-107) MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java (+26/-2) MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java (+17/-14) MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java (+215/-0) MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java (+22/-15) MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java (+7/-3) MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java (+56/-0) MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatCustomPropertyChecker.java (+2/-2) MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java (+0/-7) MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java (+5/-6) MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java (+59/-51) MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java (+1/-1) STGPlugin/src/org/workcraft/plugins/stg/STG.java (+22/-12) STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java (+11/-11) Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java (+1/-1) WorkcraftCore/src/org/workcraft/Info.java (+1/-1) WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java (+9/-9) WorkcraftCore/src/org/workcraft/gui/MainWindow.java (+2/-2) WorkcraftCore/src/org/workcraft/util/FileUtils.java (+0/-2) build_distr_linux.sh (+1/-1) build_distr_windows.sh (+1/-1) |
To merge this branch: | bzr merge lp:~danilovesky/workcraft/trunk-stg-conformation |
Related bugs: | |
Related blueprints: |
Improve STG usability
(Low)
|
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.
- 575. By Danil Sokolov
-
Polishing the Reach expression for conformation check.
Revision history for this message
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Danil Sokolov (danilovesky) : | # |
review:
Needs Resubmitting
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/tasks/CheckCircuitTask.java' |
2 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java 2014-11-24 15:37:13 +0000 |
3 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java 2014-11-30 23:14:46 +0000 |
4 | @@ -1,6 +1,13 @@ |
5 | package org.workcraft.plugins.circuit.tasks; |
6 | |
7 | +import java.io.BufferedReader; |
8 | +import java.io.ByteArrayInputStream; |
9 | import java.io.File; |
10 | +import java.io.IOException; |
11 | +import java.io.InputStream; |
12 | +import java.io.InputStreamReader; |
13 | +import java.util.HashSet; |
14 | +import java.util.Set; |
15 | |
16 | import org.workcraft.Framework; |
17 | import org.workcraft.interop.Exporter; |
18 | @@ -14,10 +21,11 @@ |
19 | import org.workcraft.plugins.mpsat.tasks.MpsatChainTask; |
20 | import org.workcraft.plugins.mpsat.tasks.MpsatTask; |
21 | import org.workcraft.plugins.mpsat.tasks.PunfTask; |
22 | -import org.workcraft.plugins.pcomp.PCompOutputMode; |
23 | import org.workcraft.plugins.pcomp.tasks.PcompTask; |
24 | +import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode; |
25 | import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
26 | import org.workcraft.plugins.stg.STG; |
27 | +import org.workcraft.plugins.stg.SignalTransition.Type; |
28 | import org.workcraft.serialisation.Format; |
29 | import org.workcraft.tasks.ProgressMonitor; |
30 | import org.workcraft.tasks.Result; |
31 | @@ -62,6 +70,7 @@ |
32 | |
33 | @Override |
34 | public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
35 | + File workingDirectory = null; |
36 | try { |
37 | // Common variables |
38 | monitor.progressUpdate(0.05); |
39 | @@ -70,79 +79,76 @@ |
40 | title = title.substring(0, title.length() - 5); |
41 | } |
42 | VisualCircuit visualCircuit = (VisualCircuit)we.getModelEntry().getVisualModel(); |
43 | - STG circuitStg = (STG)STGGenerator.generate(visualCircuit).getMathModel(); |
44 | - Exporter stgExporter = Export.chooseBestExporter(framework.getPluginManager(), circuitStg, Format.STG); |
45 | - if (stgExporter == null) { |
46 | - throw new RuntimeException ("Exporter not available: model class " + circuitStg.getClass().getName() + " to format STG."); |
47 | + File envFile = visualCircuit.getEnvironmentFile(); |
48 | + boolean hasEnvironment = ((envFile != null) && envFile.exists()); |
49 | + |
50 | + workingDirectory = FileUtils.createTempDirectory(title + "-"); |
51 | + |
52 | + STG devStg = (STG)STGGenerator.generate(visualCircuit).getMathModel(); |
53 | + Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG); |
54 | + if (devStgExporter == null) { |
55 | + throw new RuntimeException ("Exporter not available: model class " + devStg.getClass().getName() + " to format STG."); |
56 | } |
57 | SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor); |
58 | monitor.progressUpdate(0.10); |
59 | |
60 | // Generating .g for the circuit |
61 | - String circuitFilePrefix = title + "-circuit-"; |
62 | - File circuitStgFile = File.createTempFile(circuitFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion()); |
63 | - ExportTask circuitExportTask = new ExportTask(stgExporter, circuitStg, circuitStgFile.getCanonicalPath()); |
64 | - Result<? extends Object> circuitExportResult = framework.getTaskManager().execute( |
65 | - circuitExportTask, "Exporting circuit .g", subtaskMonitor); |
66 | + String devStgName = (hasEnvironment ? "dev.g" : "system.g"); |
67 | + File devStgFile = new File(workingDirectory, devStgName); |
68 | + ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath()); |
69 | + Result<? extends Object> devExportResult = framework.getTaskManager().execute( |
70 | + devExportTask, "Exporting circuit .g", subtaskMonitor); |
71 | |
72 | - if (circuitExportResult.getOutcome() != Outcome.FINISHED) { |
73 | - circuitStgFile.delete(); |
74 | - if (circuitExportResult.getOutcome() == Outcome.CANCELLED) { |
75 | + if (devExportResult.getOutcome() != Outcome.FINISHED) { |
76 | + if (devExportResult.getOutcome() == Outcome.CANCELLED) { |
77 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
78 | } |
79 | return new Result<MpsatChainResult>(Outcome.FAILED, |
80 | - new MpsatChainResult(circuitExportResult, null, null, null, toolchainPreparationSettings)); |
81 | + new MpsatChainResult(devExportResult, null, null, null, toolchainPreparationSettings)); |
82 | } |
83 | monitor.progressUpdate(0.20); |
84 | |
85 | // Generating .g for the environment |
86 | - File stgFile; |
87 | STG stg; |
88 | + File stgFile = null; |
89 | Result<? extends ExternalProcessResult> pcompResult = null; |
90 | - File environmentFile = visualCircuit.getEnvironmentFile(); |
91 | - boolean hasEnvironment = ((environmentFile != null) && environmentFile.exists()); |
92 | if ( !hasEnvironment ) { |
93 | - // No environment to compose with |
94 | - stgFile = circuitStgFile; |
95 | - stg = circuitStg; |
96 | + stgFile = devStgFile; |
97 | + stg = devStg; |
98 | } else { |
99 | - // Compose circuit with its environment |
100 | - File environmentStgFile; |
101 | - if (environmentFile.getName().endsWith(".g")) { |
102 | - environmentStgFile = environmentFile; |
103 | + File envStgFile = null; |
104 | + if (envFile.getName().endsWith(".g")) { |
105 | + envStgFile = envFile; |
106 | } else { |
107 | - STG environementStg = (STG)framework.loadFile(environmentFile).getMathModel(); |
108 | - String environmentFilePrefix = title + "-environment-"; |
109 | - environmentStgFile = File.createTempFile(environmentFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion()); |
110 | - ExportTask environmentExportTask = new ExportTask(stgExporter, environementStg, environmentStgFile.getCanonicalPath()); |
111 | - Result<? extends Object> environmentExportResult = framework.getTaskManager().execute( |
112 | - environmentExportTask, "Exporting environment .g", subtaskMonitor); |
113 | + STG envStg = (STG)framework.loadFile(envFile).getMathModel(); |
114 | + Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG); |
115 | + envStgFile = new File(workingDirectory, "env.g"); |
116 | + ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath()); |
117 | + Result<? extends Object> envExportResult = framework.getTaskManager().execute( |
118 | + envExportTask, "Exporting environment .g", subtaskMonitor); |
119 | |
120 | - if (environmentExportResult.getOutcome() != Outcome.FINISHED) { |
121 | - environmentStgFile.delete(); |
122 | - if (environmentExportResult.getOutcome() == Outcome.CANCELLED) { |
123 | + if (envExportResult.getOutcome() != Outcome.FINISHED) { |
124 | + if (envExportResult.getOutcome() == Outcome.CANCELLED) { |
125 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
126 | } |
127 | return new Result<MpsatChainResult>(Outcome.FAILED, |
128 | - new MpsatChainResult(environmentExportResult, null, null, null, toolchainPreparationSettings)); |
129 | + new MpsatChainResult(envExportResult, null, null, null, toolchainPreparationSettings)); |
130 | } |
131 | } |
132 | monitor.progressUpdate(0.25); |
133 | |
134 | // Generating .g for the whole system (circuit and environment) |
135 | - String systemFilePrefix = title + "-system-"; |
136 | - stgFile = File.createTempFile(systemFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion()); |
137 | - PcompTask pcompTask = new PcompTask(new File[]{circuitStgFile, environmentStgFile}, PCompOutputMode.OUTPUT, true, false); |
138 | + stgFile = new File(workingDirectory, "system.g"); |
139 | + PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, ConversionMode.OUTPUT, true, false, workingDirectory); |
140 | pcompResult = framework.getTaskManager().execute( |
141 | pcompTask, "Running pcomp", subtaskMonitor); |
142 | |
143 | if (pcompResult.getOutcome() != Outcome.FINISHED) { |
144 | - circuitStgFile.delete(); |
145 | if (pcompResult.getOutcome() == Outcome.CANCELLED) { |
146 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
147 | } |
148 | return new Result<MpsatChainResult>(Outcome.FAILED, |
149 | - new MpsatChainResult(circuitExportResult, pcompResult, null, null, toolchainPreparationSettings)); |
150 | + new MpsatChainResult(devExportResult, pcompResult, null, null, toolchainPreparationSettings)); |
151 | } |
152 | FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput())); |
153 | WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true); |
154 | @@ -151,26 +157,26 @@ |
155 | monitor.progressUpdate(0.30); |
156 | |
157 | // Generate unfolding |
158 | - String unfoldingFilePrefix = title + "-unfolding-"; |
159 | - File unfoldingFile = File.createTempFile(unfoldingFilePrefix.replaceAll("\\s",""), MpsatUtilitySettings.getUnfoldingExtension()); |
160 | + File unfoldingFile = new File(workingDirectory, "system" + MpsatUtilitySettings.getUnfoldingExtension()); |
161 | PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath()); |
162 | Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
163 | punfTask, "Unfolding .g", subtaskMonitor); |
164 | |
165 | - stgFile.delete(); |
166 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
167 | - unfoldingFile.delete(); |
168 | if (punfResult.getOutcome() == Outcome.CANCELLED) { |
169 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
170 | } |
171 | return new Result<MpsatChainResult>(Outcome.FAILED, |
172 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainPreparationSettings)); |
173 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainPreparationSettings)); |
174 | } |
175 | monitor.progressUpdate(0.40); |
176 | |
177 | // Check for interface conformation (only if the environment is specified) |
178 | if (hasEnvironment && checkConformation) { |
179 | - String reachConformation = MpsatSettings.genReachConformation(stg, circuitStg); |
180 | + Set<String> devOutputNames = devStg.getSignalFlatNames(Type.OUTPUT); |
181 | + Set<String> devPlaceNames = parsePlaceNames(pcompResult.getReturnValue().getOutputFile("places.list"), 0); |
182 | +// String reachConformation = MpsatSettings.genReachConformation(devOutputNames, devPlaceNames); |
183 | + String reachConformation = MpsatSettings.genReachConformationDetail(stg, devOutputNames, devPlaceNames); |
184 | if (MpsatUtilitySettings.getDebugReach()) { |
185 | System.out.println("\nReach expression for the interface conformation property:"); |
186 | System.out.println(reachConformation); |
187 | @@ -179,7 +185,8 @@ |
188 | MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), |
189 | MpsatUtilitySettings.getSolutionCount(), reachConformation); |
190 | |
191 | - MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath()); |
192 | + MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), |
193 | + unfoldingFile.getCanonicalPath(), workingDirectory); |
194 | Result<? extends ExternalProcessResult> mpsatConformationResult = framework.getTaskManager().execute( |
195 | mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor); |
196 | |
197 | @@ -188,15 +195,14 @@ |
198 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
199 | } |
200 | return new Result<MpsatChainResult>(Outcome.FAILED, |
201 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings)); |
202 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings)); |
203 | } |
204 | monitor.progressUpdate(0.50); |
205 | |
206 | MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue()); |
207 | if (!mpsatConformationParser.getSolutions().isEmpty()) { |
208 | - unfoldingFile.delete(); |
209 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
210 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, |
211 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, |
212 | "Circuit does not conform to the environment after the following trace:")); |
213 | } |
214 | } |
215 | @@ -204,7 +210,8 @@ |
216 | |
217 | // Check for deadlock |
218 | if (checkDeadlock) { |
219 | - MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath()); |
220 | + MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), |
221 | + unfoldingFile.getCanonicalPath(), workingDirectory); |
222 | Result<? extends ExternalProcessResult> mpsatDeadlockResult = framework.getTaskManager().execute( |
223 | mpsatDeadlockTask, "Running deadlock check [MPSat]", subtaskMonitor); |
224 | |
225 | @@ -213,15 +220,14 @@ |
226 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
227 | } |
228 | return new Result<MpsatChainResult>(Outcome.FAILED, |
229 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings)); |
230 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings)); |
231 | } |
232 | monitor.progressUpdate(0.70); |
233 | |
234 | MpsatResultParser mpsatDeadlockParser = new MpsatResultParser(mpsatDeadlockResult.getReturnValue()); |
235 | if (!mpsatDeadlockParser.getSolutions().isEmpty()) { |
236 | - unfoldingFile.delete(); |
237 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
238 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, |
239 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, |
240 | "Circuit has a deadlock after the following trace:")); |
241 | } |
242 | } |
243 | @@ -229,7 +235,8 @@ |
244 | |
245 | // Check for hazards |
246 | if (checkHazard) { |
247 | - MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath()); |
248 | + MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), |
249 | + unfoldingFile.getCanonicalPath(), workingDirectory); |
250 | if (MpsatUtilitySettings.getDebugReach()) { |
251 | System.out.println("\nReach expression for the hazard property:"); |
252 | System.out.println(hazardSettings.getReach()); |
253 | @@ -242,44 +249,72 @@ |
254 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
255 | } |
256 | return new Result<MpsatChainResult>(Outcome.FAILED, |
257 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings)); |
258 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings)); |
259 | } |
260 | monitor.progressUpdate(0.90); |
261 | |
262 | MpsatResultParser mpsatHazardParser = new MpsatResultParser(mpsatHazardResult.getReturnValue()); |
263 | if (!mpsatHazardParser.getSolutions().isEmpty()) { |
264 | - unfoldingFile.delete(); |
265 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
266 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, |
267 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, |
268 | "Circuit has a hazard after the following trace:")); |
269 | } |
270 | } |
271 | monitor.progressUpdate(1.0); |
272 | |
273 | // Success |
274 | - unfoldingFile.delete(); |
275 | - String message = ""; |
276 | - if (hasEnvironment) { |
277 | - message = "Under the given environment (" + environmentFile.getName() + ")"; |
278 | - } else { |
279 | - message = "Without environment restrictions"; |
280 | - } |
281 | - message += " the circuit is:\n"; |
282 | - if (checkConformation) { |
283 | - message += " * conformant\n"; |
284 | - } |
285 | - if (checkDeadlock) { |
286 | - message += " * deadlock-free\n"; |
287 | - } |
288 | - if (checkHazard) { |
289 | - message += " * hazard-free\n"; |
290 | - } |
291 | + String message = getSuccessMessage(envFile); |
292 | return new Result<MpsatChainResult>(Outcome.FINISHED, |
293 | - new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message)); |
294 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message)); |
295 | |
296 | } catch (Throwable e) { |
297 | return new Result<MpsatChainResult>(e); |
298 | - } |
299 | + } finally { |
300 | + if ((workingDirectory != null) && !MpsatUtilitySettings.getDebugTemporaryFiles()) { |
301 | + FileUtils.deleteDirectoryTree(workingDirectory); |
302 | + } |
303 | + } |
304 | + } |
305 | + |
306 | + private HashSet<String> parsePlaceNames(byte[] bufferedInput, int lineIndex) { |
307 | + HashSet<String> result = new HashSet<String>(); |
308 | + InputStream is = new ByteArrayInputStream(bufferedInput); |
309 | + BufferedReader br = new BufferedReader(new InputStreamReader(is)); |
310 | + try { |
311 | + String line = null; |
312 | + while ((lineIndex >= 0) && ((line = br.readLine()) != null)) { |
313 | + lineIndex--; |
314 | + } |
315 | + if (line != null) { |
316 | + for (String name: line.trim().split("\\s")) { |
317 | + result.add(name); |
318 | + } |
319 | + } |
320 | + } catch (IOException e) { |
321 | + e.printStackTrace(); |
322 | + } |
323 | + return result; |
324 | + } |
325 | + |
326 | + private String getSuccessMessage(File environmentFile) { |
327 | + String message = ""; |
328 | + boolean hasEnvironment = ((environmentFile != null) && environmentFile.exists()); |
329 | + if (hasEnvironment) { |
330 | + message = "Under the given environment (" + environmentFile.getName() + ")"; |
331 | + } else { |
332 | + message = "Without environment restrictions"; |
333 | + } |
334 | + message += " the circuit is:\n"; |
335 | + if (checkConformation) { |
336 | + message += " * conformant\n"; |
337 | + } |
338 | + if (checkDeadlock) { |
339 | + message += " * deadlock-free\n"; |
340 | + } |
341 | + if (checkHazard) { |
342 | + message += " * hazard-free\n"; |
343 | + } |
344 | + return message; |
345 | } |
346 | |
347 | } |
348 | |
349 | === modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java' |
350 | --- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java 2014-11-21 18:25:23 +0000 |
351 | +++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java 2014-11-30 23:14:46 +0000 |
352 | @@ -451,7 +451,7 @@ |
353 | Node parent = contact.getParent(); |
354 | if (parent instanceof VisualFunctionComponent) { |
355 | VisualFunctionComponent component = (VisualFunctionComponent)parent; |
356 | - String componentName = NamespaceHelper.getFlatName(circuit.getMathName(component)); |
357 | + String componentName = NamespaceHelper.hierarchicalToFlatName(circuit.getMathName(component)); |
358 | String contactName = circuit.getMathName(contact); |
359 | result = componentName + "_" + contactName; |
360 | } |
361 | @@ -470,7 +470,7 @@ |
362 | result = circuit.getMathName(outputPort); |
363 | } else { |
364 | // If the component has a single output, use the component name. Otherwise append the contact. |
365 | - result = NamespaceHelper.getFlatName(circuit.getMathName(component)); |
366 | + result = NamespaceHelper.hierarchicalToFlatName(circuit.getMathName(component)); |
367 | int output_cnt = 0; |
368 | for (Node node: component.getChildren()) { |
369 | if (node instanceof VisualContact) { |
370 | |
371 | === modified file 'CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java' |
372 | --- CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java 2014-07-11 09:35:42 +0000 |
373 | +++ CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java 2014-11-30 23:14:46 +0000 |
374 | @@ -61,7 +61,7 @@ |
375 | |
376 | String ref = internalReferences.getReference(node); |
377 | // use full path to a flattened name |
378 | - String flat = NamespaceHelper.getFlatName(ref); |
379 | + String flat = NamespaceHelper.hierarchicalToFlatName(ref); |
380 | |
381 | // old style naming, if number is used as an ID for a contact |
382 | if (Identifier.isNumber(ref)) { |
383 | |
384 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java' |
385 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java 2013-09-18 16:19:20 +0000 |
386 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java 2014-11-30 23:14:46 +0000 |
387 | @@ -28,12 +28,11 @@ |
388 | this.result = result; |
389 | } |
390 | |
391 | - public STGModel getResolvedStg() |
392 | - { |
393 | + public STGModel getResolvedStg() { |
394 | final byte[] output = result.getReturnValue().getMpsatResult().getReturnValue().getOutputFile("mpsat.g"); |
395 | - if(output == null) |
396 | + if(output == null) { |
397 | return null; |
398 | - |
399 | + } |
400 | try { |
401 | return new DotGImporter().importSTG(new ByteArrayInputStream(output)); |
402 | } catch (DeserialisationException e) { |
403 | |
404 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java' |
405 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java 2014-10-24 16:33:38 +0000 |
406 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java 2014-11-30 23:14:46 +0000 |
407 | @@ -6,13 +6,13 @@ |
408 | import org.workcraft.Tool; |
409 | import org.workcraft.gui.propertyeditor.Settings; |
410 | import org.workcraft.plugins.mpsat.tools.CscResolutionTool; |
411 | -import org.workcraft.plugins.mpsat.tools.CustomPropertyMpsatChecker; |
412 | +import org.workcraft.plugins.mpsat.tools.MpsatConformationChecker; |
413 | import org.workcraft.plugins.mpsat.tools.MpsatConsistencyChecker; |
414 | import org.workcraft.plugins.mpsat.tools.MpsatCscChecker; |
415 | +import org.workcraft.plugins.mpsat.tools.MpsatCustomPropertyChecker; |
416 | import org.workcraft.plugins.mpsat.tools.MpsatDeadlockChecker; |
417 | import org.workcraft.plugins.mpsat.tools.MpsatNormalcyChecker; |
418 | import org.workcraft.plugins.mpsat.tools.MpsatPersistencyChecker; |
419 | -import org.workcraft.plugins.mpsat.tools.MpsatSynthesis; |
420 | import org.workcraft.plugins.mpsat.tools.MpsatSynthesisComplexGate; |
421 | import org.workcraft.plugins.mpsat.tools.MpsatSynthesisGeneralisedCelement; |
422 | import org.workcraft.plugins.mpsat.tools.MpsatSynthesisStandardCelement; |
423 | @@ -38,7 +38,8 @@ |
424 | p.registerClass(Tool.class, MpsatNormalcyChecker.class, framework); |
425 | p.registerClass(Tool.class, MpsatCscChecker.class, framework); |
426 | p.registerClass(Tool.class, MpsatUscChecker.class, framework); |
427 | - p.registerClass(Tool.class, CustomPropertyMpsatChecker.class, framework); |
428 | + p.registerClass(Tool.class, MpsatConformationChecker.class, framework); |
429 | + p.registerClass(Tool.class, MpsatCustomPropertyChecker.class, framework); |
430 | |
431 | p.registerClass(Settings.class, MpsatUtilitySettings.class); |
432 | p.registerClass(Settings.class, PunfUtilitySettings.class); |
433 | |
434 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java' |
435 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java 2014-11-13 00:05:09 +0000 |
436 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java 2014-11-30 23:14:46 +0000 |
437 | @@ -6,9 +6,10 @@ |
438 | import java.io.File; |
439 | import java.io.IOException; |
440 | import java.util.ArrayList; |
441 | -import java.util.HashSet; |
442 | +import java.util.Collection; |
443 | import java.util.LinkedHashMap; |
444 | import java.util.Map; |
445 | +import java.util.Set; |
446 | import java.util.regex.Matcher; |
447 | import java.util.regex.Pattern; |
448 | |
449 | @@ -16,7 +17,7 @@ |
450 | import org.workcraft.dom.hierarchy.NamespaceHelper; |
451 | import org.workcraft.plugins.stg.STG; |
452 | import org.workcraft.plugins.stg.SignalTransition; |
453 | -import org.workcraft.plugins.stg.SignalTransition.Type; |
454 | +import org.workcraft.plugins.stg.SignalTransition.Direction; |
455 | import org.workcraft.util.FileUtils; |
456 | |
457 | public class MpsatSettings { |
458 | @@ -53,134 +54,158 @@ |
459 | // Reach expression for checking signal consistency |
460 | public static final String reachConsistency = |
461 | "exists s in SIGNALS \\ DUMMY {\n" + |
462 | - " let Es = ev s {\n" + |
463 | - " $s & exists e in Es s.t. is_plus e { @e }\n" + |
464 | - " |\n" + |
465 | - " ~$s & exists e in Es s.t. is_minus e { @e }\n" + |
466 | - " }\n" + |
467 | + " let Es = ev s {\n" + |
468 | + " $s & exists e in Es s.t. is_plus e { @e }\n" + |
469 | + " |\n" + |
470 | + " ~$s & exists e in Es s.t. is_minus e { @e }\n" + |
471 | + " }\n" + |
472 | "}\n"; |
473 | |
474 | // Reach expression for checking semimodularity (output persistency) |
475 | public static final String reachSemimodularity = |
476 | "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" + |
477 | - " exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n" + |
478 | - " @t1 &\n" + |
479 | - " exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n" + |
480 | - " @t2 &\n" + |
481 | - " forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n" + |
482 | - " exists p in pre t3 \\ post t2 { ~$p }\n" + |
483 | - " }\n" + |
484 | - " }\n" + |
485 | - " }\n"; |
486 | + " exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n" + |
487 | + " @t1 &\n" + |
488 | + " exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n" + |
489 | + " @t2 &\n" + |
490 | + " forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n" + |
491 | + " exists p in pre t3 \\ post t2 { ~$p }\n" + |
492 | + " }\n" + |
493 | + " }\n" + |
494 | + " }\n"; |
495 | |
496 | // Reach expression for checking conformation (this is a template, |
497 | // the list of places needs to be updated for each circuit) |
498 | public static final String reachConformation = |
499 | - "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" + |
500 | - " let CPnames = {\"in1_0\", \"in1_1\", \"in0_0\", \"in0_1\", \"out0_0\", \"out0_1\"},\n" + |
501 | - " CP=gather n in CPnames { P n } {\n" + |
502 | - " exists s in SIGNALS \\ DUMMY {\n" + |
503 | - " exists t in tran s {\n" + |
504 | - " forall p in pre t * CP { $p }\n" + |
505 | - " }\n" + |
506 | - " &\n" + |
507 | - " forall t in tran s {\n" + |
508 | - " exists p in pre t \\ CP { ~$p }\n" + |
509 | - " }\n" + |
510 | - " }\n" + |
511 | - " }\n"; |
512 | - |
513 | +// "let devOutputs = gather signalName in { \"out0\" } { S signalName },\n" + |
514 | +// " devPlaces = gather placeName in { \"in1_0\", \"in1_1\", \"in0_1\", \"in0_0\", \"<out0+,out0->\", \"<out0-,out0+>\" } { P placeName } {\n" + |
515 | + " card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" + |
516 | + " exists s in devOutputs {\n" + |
517 | + " exists t in tran s {\n" + |
518 | + " is_plus t & forall p in pre t * devPlaces { $ p }\n" + |
519 | + " }\n" + |
520 | + " &\n" + |
521 | + " forall t in tran s {\n" + |
522 | + " is_plus t & exists p in pre t \\ devPlaces { ~ $ p }\n" + |
523 | + " }\n" + |
524 | + " |\n" + |
525 | + " exists t in tran s {\n" + |
526 | + " is_minus t & forall p in pre t * devPlaces { $ p }\n" + |
527 | + " }\n" + |
528 | + " &\n" + |
529 | + " forall t in tran s {\n" + |
530 | + " is_minus t & exists p in pre t \\ devPlaces { ~ $ p }\n" + |
531 | + " }\n" + |
532 | + " }\n" + |
533 | + "}\n"; |
534 | + |
535 | // Note: New (PNML-based) version of Punf is required to check conformation property. |
536 | // Old version of Punf does not support dead signals, transitions and places well |
537 | // (e.g. a dead transition may disappear from unfolding), therefore the conformation |
538 | // property cannot be checked reliably. |
539 | - public static String genReachConformation(STG stg, STG circuitStg) { |
540 | - // Form a set of system STG places which came from the circuitStg |
541 | - HashSet<Node> circuitPlaces = new HashSet<Node>(); |
542 | - for (Type type: Type.values()) { |
543 | - for (String s : circuitStg.getSignalReferences(type)) { |
544 | - Node p0 = stg.getNodeByReference(s + "_0"); |
545 | - if (p0 == null) { |
546 | - p0 = stg.getNodeByReference("<" + s + "-," + s + "+>"); |
547 | - } |
548 | - if (p0 != null) { |
549 | - circuitPlaces.add(p0); |
550 | - } |
551 | - Node p1 = stg.getNodeByReference(s + "_1"); |
552 | - if (p1 == null) { |
553 | - p1 = stg.getNodeByReference("<" + s + "+," + s + "->"); |
554 | - } |
555 | - if (p1 != null) { |
556 | - circuitPlaces.add(p1); |
557 | - } |
558 | + public static String genReachConformation(Set<String> devOutputNames, Set<String> devPlaceNames) { |
559 | + String devOutputList = genNameList(devOutputNames); |
560 | + String devPlaceList = genNameList(devPlaceNames); |
561 | + return "let devOutputs = gather signalName in { " + devOutputList + " } { S signalName },\n" + |
562 | + " devPlaces = gather placeName in { " + devPlaceList + " } { P placeName } {\n" + |
563 | + reachConformation; |
564 | + } |
565 | + |
566 | + private static String genNameList(Collection<String> names) { |
567 | + String result = ""; |
568 | + for (String name: names) { |
569 | + if ( !result.isEmpty() ) { |
570 | + result += ", "; |
571 | } |
572 | + result += "\"" + name + "\""; |
573 | } |
574 | - // Generate Reach expression |
575 | + return result; |
576 | + } |
577 | + |
578 | + public static String genReachConformationDetail(STG stg, Set<String> devOutputNames, Set<String> devPlaceNames) { |
579 | String result = ""; |
580 | - for (String s : circuitStg.getSignalReferences(Type.OUTPUT)) { |
581 | - String circuitPredicate = ""; |
582 | - String environmentPredicate = ""; |
583 | - for (SignalTransition t: stg.getSignalTransitions()) { |
584 | - if (!t.getSignalType().equals(Type.OUTPUT) || !t.getSignalName().equals(s)) continue; |
585 | - String circuitPreset = ""; |
586 | - String environmentPreset = ""; |
587 | + for (String signalFlatName: devOutputNames) { |
588 | + String riseDevPredicate = ""; |
589 | + String fallDevPredicate = ""; |
590 | + String riseEnvPredicate = ""; |
591 | + String fallEnvPredicate = ""; |
592 | + |
593 | + String signalRef = NamespaceHelper.flatToHierarchicalName(signalFlatName); |
594 | + for (SignalTransition t: stg.getSignalTransitions(signalRef)) { |
595 | + String devPreset = ""; |
596 | + String envPreset = ""; |
597 | for (Node p: stg.getPreset(t)) { |
598 | - String name = stg.getNodeReference(p); |
599 | - if (circuitPlaces.contains(p)) { |
600 | - if (circuitPreset.isEmpty()) { |
601 | - circuitPreset += "{"; |
602 | - } else { |
603 | - circuitPreset += ", "; |
604 | - } |
605 | - circuitPreset += "\"" + name + "\""; |
606 | + String placeRef = stg.getNodeReference(p); |
607 | + String placeFlatName = NamespaceHelper.hierarchicalToFlatName(placeRef); |
608 | + if (devPlaceNames.contains(placeFlatName)) { |
609 | + devPreset += (devPreset.isEmpty() ? "{" : ", "); |
610 | + devPreset += "\"" + placeFlatName + "\""; |
611 | + } |
612 | + envPreset += (envPreset.isEmpty() ? "{" : ", "); |
613 | + envPreset += "\"" + placeFlatName + "\""; |
614 | + } |
615 | + |
616 | + if ( !devPreset.isEmpty() && !envPreset.isEmpty() ) { |
617 | + devPreset += "}"; |
618 | + envPreset += "}"; |
619 | + String devPredicate = ""; |
620 | + devPredicate += " forall p in " + devPreset + " {\n"; |
621 | + devPredicate += " $ P p\n"; |
622 | + devPredicate += " }\n"; |
623 | + String envPredicate = ""; |
624 | + envPredicate += " exists p in " + envPreset + " {\n"; |
625 | + envPredicate += " ~$ P p\n"; |
626 | + envPredicate += " }\n"; |
627 | + if (t.getDirection() == Direction.PLUS) { |
628 | + if ( !riseDevPredicate.isEmpty() ) { |
629 | + riseDevPredicate += " |\n"; |
630 | + } |
631 | + riseDevPredicate += devPredicate; |
632 | + if ( !riseEnvPredicate.isEmpty() ) { |
633 | + riseEnvPredicate += " &\n"; |
634 | + } |
635 | + riseEnvPredicate += envPredicate; |
636 | } else { |
637 | - if (environmentPreset.isEmpty()) { |
638 | - environmentPreset += "{"; |
639 | - } else { |
640 | - environmentPreset += ", "; |
641 | - } |
642 | - environmentPreset += "\"" + name + "\""; |
643 | + if ( !fallDevPredicate.isEmpty() ) { |
644 | + fallDevPredicate += " |\n"; |
645 | + } |
646 | + fallDevPredicate += devPredicate; |
647 | + if ( !fallEnvPredicate.isEmpty() ) { |
648 | + fallEnvPredicate += " &\n"; |
649 | + } |
650 | + fallEnvPredicate += envPredicate; |
651 | } |
652 | } |
653 | - circuitPreset += "}"; |
654 | - environmentPreset += "}"; |
655 | - |
656 | - if (circuitPredicate.isEmpty()) { |
657 | - circuitPredicate += " (\n"; |
658 | - } else { |
659 | - circuitPredicate += " |\n"; |
660 | - } |
661 | - circuitPredicate += " forall p in " + circuitPreset + " {\n"; |
662 | - circuitPredicate += " $ P p\n"; |
663 | - circuitPredicate += " }\n"; |
664 | - |
665 | - if (environmentPredicate.isEmpty()) { |
666 | - environmentPredicate += " (\n"; |
667 | - } else { |
668 | - environmentPredicate += " &\n"; |
669 | - } |
670 | - environmentPredicate += " exists p in " + environmentPreset + " {\n"; |
671 | - environmentPredicate += " ~$ P p\n"; |
672 | - environmentPredicate += " }\n"; |
673 | - } |
674 | - circuitPredicate += " )\n"; |
675 | - environmentPredicate += " )\n"; |
676 | - if (result.isEmpty()) { |
677 | - result = "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n"; |
678 | - } else { |
679 | - result += "|\n"; |
680 | - } |
681 | - result += "/* Conformation check for signal " + s + " */\n"; |
682 | - result += "(\n"; |
683 | - result += circuitPredicate; |
684 | - result += " &\n"; |
685 | - result += environmentPredicate; |
686 | - result += ")\n"; |
687 | + } |
688 | + |
689 | + if ( !riseDevPredicate.isEmpty() || !fallDevPredicate.isEmpty() ) { |
690 | + if (result.isEmpty()) { |
691 | + result = "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n"; |
692 | + } else { |
693 | + result += "|\n"; |
694 | + } |
695 | + result += "( /* Conformation check for signal \"" + signalFlatName + "\" */\n"; |
696 | + result += " (\n"; |
697 | + result += riseDevPredicate; |
698 | + result += " )\n"; |
699 | + result += " &\n"; |
700 | + result += " (\n"; |
701 | + result += riseEnvPredicate; |
702 | + result += " )\n"; |
703 | + result += " |\n"; |
704 | + result += " (\n"; |
705 | + result += fallDevPredicate; |
706 | + result += " )\n"; |
707 | + result += " &\n"; |
708 | + result += " (\n"; |
709 | + result += fallEnvPredicate; |
710 | + result += " )\n"; |
711 | + result += ")\n"; |
712 | + } |
713 | } |
714 | return result; |
715 | } |
716 | |
717 | - |
718 | public MpsatSettings(String name, MpsatMode mode, int verbosity, SolutionMode solutionMode, int solutionNumberLimit, String reach) { |
719 | super(); |
720 | this.name = name; |
721 | @@ -212,7 +237,7 @@ |
722 | Matcher matcher = nodeNamePattern.matcher(reach); |
723 | while (matcher.find()) { |
724 | String reference = matcher.group(1); |
725 | - String flatName = NamespaceHelper.getFlatName(reference); |
726 | + String flatName = NamespaceHelper.hierarchicalToFlatName(reference); |
727 | matcher.appendReplacement(sb, "\"" + flatName + "\""); |
728 | } |
729 | matcher.appendTail(sb); |
730 | |
731 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java' |
732 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java 2014-09-05 16:36:36 +0000 |
733 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java 2014-11-30 23:14:46 +0000 |
734 | @@ -38,18 +38,21 @@ |
735 | private static final String keyExtraArgs = prefix + ".args"; |
736 | private static final String keyUsePnmlUnfolding = prefix + ".usePnmlUnfolding"; |
737 | private static final String keyDebugReach = prefix + ".debugReach"; |
738 | + private static final String keyDebugTemporaryFiles = prefix + ".debugTemporaryFiles"; |
739 | |
740 | private static final String defaultCommand = "mpsat"; |
741 | private static final SolutionMode defaultSolutionMode = SolutionMode.MINIMUM_COST; |
742 | private static final String defaultExtraArgs = ""; |
743 | private static final Boolean defaultUsePnmlUnfolding = false; |
744 | private static final Boolean defaultDebugReach = false; |
745 | + private static final Boolean defaultDebugTemporaryFiles = true; |
746 | |
747 | private static String command = defaultCommand; |
748 | private static SolutionMode solutionMode = defaultSolutionMode; |
749 | private static String extraArgs = defaultExtraArgs; |
750 | private static Boolean usePnmlUnfolding = defaultUsePnmlUnfolding; |
751 | private static Boolean debugReach = defaultDebugReach; |
752 | + private static Boolean debigTemporaryFiles = defaultDebugTemporaryFiles; |
753 | |
754 | public MpsatUtilitySettings() { |
755 | properties.add(new PropertyDeclaration<MpsatUtilitySettings, String>( |
756 | @@ -93,7 +96,7 @@ |
757 | }); |
758 | |
759 | properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>( |
760 | - this, "Debug Reach expressions", Boolean.class) { |
761 | + this, "Print out Reach expressions (debug)", Boolean.class) { |
762 | protected void setter(MpsatUtilitySettings object, Boolean value) { |
763 | MpsatUtilitySettings.setDebugReach(value); |
764 | } |
765 | @@ -101,6 +104,16 @@ |
766 | return MpsatUtilitySettings.getDebugReach(); |
767 | } |
768 | }); |
769 | + |
770 | + properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>( |
771 | + this, "Keep temporary files (debug)", Boolean.class) { |
772 | + protected void setter(MpsatUtilitySettings object, Boolean value) { |
773 | + MpsatUtilitySettings.setDebugTemporaryFiles(value); |
774 | + } |
775 | + protected Boolean getter(MpsatUtilitySettings object) { |
776 | + return MpsatUtilitySettings.getDebugTemporaryFiles(); |
777 | + } |
778 | + }); |
779 | } |
780 | |
781 | @Override |
782 | @@ -115,6 +128,7 @@ |
783 | setExtraArgs(config.getString(keyExtraArgs, defaultExtraArgs)); |
784 | setUsePnmlUnfolding(config.getBoolean(keyUsePnmlUnfolding, defaultUsePnmlUnfolding)); |
785 | setDebugReach(config.getBoolean(keyDebugReach, defaultDebugReach)); |
786 | + setDebugTemporaryFiles(config.getBoolean(keyDebugTemporaryFiles, defaultDebugTemporaryFiles)); |
787 | } |
788 | |
789 | @Override |
790 | @@ -124,6 +138,8 @@ |
791 | config.set(keyExtraArgs, getExtraArgs()); |
792 | config.setBoolean(keyUsePnmlUnfolding, getUsePnmlUnfolding()); |
793 | config.setBoolean(keyDebugReach, getDebugReach()); |
794 | + config.setBoolean(keyDebugTemporaryFiles, getDebugTemporaryFiles()); |
795 | + |
796 | } |
797 | |
798 | @Override |
799 | @@ -171,7 +187,7 @@ |
800 | public static void setUsePnmlUnfolding(Boolean value) { |
801 | usePnmlUnfolding = value; |
802 | } |
803 | - |
804 | + |
805 | public static Boolean getDebugReach() { |
806 | return debugReach; |
807 | } |
808 | @@ -180,6 +196,14 @@ |
809 | debugReach = value; |
810 | } |
811 | |
812 | + public static Boolean getDebugTemporaryFiles() { |
813 | + return debigTemporaryFiles; |
814 | + } |
815 | + |
816 | + public static void setDebugTemporaryFiles(Boolean value) { |
817 | + debigTemporaryFiles = value; |
818 | + } |
819 | + |
820 | public static String getUnfoldingExtension() { |
821 | return (getUsePnmlUnfolding() ? ".pnml" : ".mci"); |
822 | } |
823 | |
824 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java' |
825 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java 2014-09-05 16:36:36 +0000 |
826 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java 2014-11-30 23:14:46 +0000 |
827 | @@ -11,44 +11,41 @@ |
828 | import org.workcraft.serialisation.Format; |
829 | import org.workcraft.tasks.ProgressMonitor; |
830 | import org.workcraft.tasks.Result; |
831 | +import org.workcraft.tasks.Result.Outcome; |
832 | import org.workcraft.tasks.SubtaskMonitor; |
833 | import org.workcraft.tasks.Task; |
834 | -import org.workcraft.tasks.Result.Outcome; |
835 | import org.workcraft.util.Export; |
836 | +import org.workcraft.util.Export.ExportTask; |
837 | import org.workcraft.util.WorkspaceUtils; |
838 | -import org.workcraft.util.Export.ExportTask; |
839 | import org.workcraft.workspace.WorkspaceEntry; |
840 | |
841 | public class MpsatChainTask implements Task<MpsatChainResult> { |
842 | private final WorkspaceEntry we; |
843 | private final MpsatSettings settings; |
844 | private final Framework framework; |
845 | - private PetriNetModel model; |
846 | |
847 | public MpsatChainTask(WorkspaceEntry we, MpsatSettings settings, Framework framework) { |
848 | this.we = we; |
849 | this.settings = settings; |
850 | this.framework = framework; |
851 | - this.model = null; |
852 | } |
853 | |
854 | @Override |
855 | public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
856 | + File netFile = null; |
857 | + File unfoldingFile = null; |
858 | try { |
859 | - if(model == null) { |
860 | - model = WorkspaceUtils.getAs(getWorkspaceEntry(), PetriNetModel.class); |
861 | - } |
862 | + PetriNetModel model = WorkspaceUtils.getAs(we, PetriNetModel.class); |
863 | Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG); |
864 | if (exporter == null) { |
865 | throw new RuntimeException ("Exporter not available: model class " + model.getClass().getName() + " to format STG."); |
866 | } |
867 | - File netFile = File.createTempFile("net", exporter.getExtenstion()); |
868 | + netFile = File.createTempFile("net", exporter.getExtenstion()); |
869 | ExportTask exportTask; |
870 | exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath()); |
871 | SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor); |
872 | Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon); |
873 | if (exportResult.getOutcome() != Outcome.FINISHED) { |
874 | - netFile.delete(); |
875 | if (exportResult.getOutcome() == Outcome.CANCELLED) { |
876 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
877 | } |
878 | @@ -56,13 +53,11 @@ |
879 | } |
880 | monitor.progressUpdate(0.33); |
881 | |
882 | - File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension()); |
883 | + unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension()); |
884 | PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath()); |
885 | Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon); |
886 | - netFile.delete(); |
887 | |
888 | if (punfResult.getOutcome() != Outcome.FINISHED) { |
889 | - unfoldingFile.delete(); |
890 | if (punfResult.getOutcome() == Outcome.CANCELLED) { |
891 | return new Result<MpsatChainResult>(Outcome.CANCELLED); |
892 | } |
893 | @@ -71,9 +66,8 @@ |
894 | |
895 | monitor.progressUpdate(0.66); |
896 | |
897 | - MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath()); |
898 | + MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null); |
899 | Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running mpsat model-checking", mon); |
900 | - unfoldingFile.delete(); |
901 | |
902 | if (mpsatResult.getOutcome() != Outcome.FINISHED) { |
903 | if (mpsatResult.getOutcome() == Outcome.CANCELLED) { |
904 | @@ -88,6 +82,15 @@ |
905 | } catch (Throwable e) { |
906 | return new Result<MpsatChainResult>(e); |
907 | } |
908 | + // Clean up |
909 | + finally { |
910 | + if ((netFile != null) && !MpsatUtilitySettings.getDebugTemporaryFiles() ) { |
911 | + netFile.delete(); |
912 | + } |
913 | + if ((unfoldingFile != null) && !MpsatUtilitySettings.getDebugTemporaryFiles() ) { |
914 | + unfoldingFile.delete(); |
915 | + } |
916 | + } |
917 | } |
918 | |
919 | public MpsatSettings getSettings() { |
920 | |
921 | === added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java' |
922 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java 1970-01-01 00:00:00 +0000 |
923 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java 2014-11-30 23:14:46 +0000 |
924 | @@ -0,0 +1,215 @@ |
925 | +package org.workcraft.plugins.mpsat.tasks; |
926 | + |
927 | +import java.io.BufferedReader; |
928 | +import java.io.ByteArrayInputStream; |
929 | +import java.io.File; |
930 | +import java.io.IOException; |
931 | +import java.io.InputStream; |
932 | +import java.io.InputStreamReader; |
933 | +import java.util.HashSet; |
934 | +import java.util.Set; |
935 | + |
936 | +import org.workcraft.Framework; |
937 | +import org.workcraft.interop.Exporter; |
938 | +import org.workcraft.plugins.mpsat.MpsatMode; |
939 | +import org.workcraft.plugins.mpsat.MpsatResultParser; |
940 | +import org.workcraft.plugins.mpsat.MpsatSettings; |
941 | +import org.workcraft.plugins.mpsat.MpsatUtilitySettings; |
942 | +import org.workcraft.plugins.pcomp.tasks.PcompTask; |
943 | +import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode; |
944 | +import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
945 | +import org.workcraft.plugins.stg.STG; |
946 | +import org.workcraft.plugins.stg.SignalTransition.Type; |
947 | +import org.workcraft.serialisation.Format; |
948 | +import org.workcraft.tasks.ProgressMonitor; |
949 | +import org.workcraft.tasks.Result; |
950 | +import org.workcraft.tasks.Result.Outcome; |
951 | +import org.workcraft.tasks.SubtaskMonitor; |
952 | +import org.workcraft.util.Export; |
953 | +import org.workcraft.util.Export.ExportTask; |
954 | +import org.workcraft.util.FileUtils; |
955 | +import org.workcraft.workspace.WorkspaceEntry; |
956 | + |
957 | + |
958 | +public class MpsatConformationTask extends MpsatChainTask { |
959 | + private final MpsatSettings toolchainPreparationSettings = new MpsatSettings("Toolchain preparation of data", |
960 | + MpsatMode.UNDEFINED, 0, null, 0, null); |
961 | + |
962 | + private final MpsatSettings toolchainCompletionSettings = new MpsatSettings("Toolchain completion", |
963 | + MpsatMode.UNDEFINED, 0, null, 0, null); |
964 | + |
965 | + private final WorkspaceEntry we; |
966 | + private final Framework framework; |
967 | + private File envFile; |
968 | + |
969 | + public MpsatConformationTask(WorkspaceEntry we, Framework framework, File envFile) { |
970 | + super (we, null, framework); |
971 | + this.we = we; |
972 | + this.framework = framework; |
973 | + this.envFile = envFile; |
974 | + } |
975 | + |
976 | + @Override |
977 | + public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) { |
978 | + File workingDirectory = null; |
979 | + try { |
980 | + // Common variables |
981 | + monitor.progressUpdate(0.10); |
982 | + String title = we.getWorkspacePath().getNode(); |
983 | + if (title.endsWith(".work")) { |
984 | + title = title.substring(0, title.length() - 5); |
985 | + } |
986 | + workingDirectory = FileUtils.createTempDirectory(title + "-"); |
987 | + |
988 | + STG devStg = (STG)we.getModelEntry().getVisualModel().getMathModel(); |
989 | + Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG); |
990 | + if (devStgExporter == null) { |
991 | + throw new RuntimeException ("Exporter not available: model class " + devStg.getClass().getName() + " to format STG."); |
992 | + } |
993 | + SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor); |
994 | + monitor.progressUpdate(0.20); |
995 | + |
996 | + // Generating .g for the model |
997 | + File devStgFile = new File(workingDirectory, "dev.g"); |
998 | + ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath()); |
999 | + Result<? extends Object> devExportResult = framework.getTaskManager().execute( |
1000 | + devExportTask, "Exporting circuit .g", subtaskMonitor); |
1001 | + |
1002 | + if (devExportResult.getOutcome() != Outcome.FINISHED) { |
1003 | + if (devExportResult.getOutcome() == Outcome.CANCELLED) { |
1004 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1005 | + } |
1006 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1007 | + new MpsatChainResult(devExportResult, null, null, null, toolchainPreparationSettings)); |
1008 | + } |
1009 | + monitor.progressUpdate(0.30); |
1010 | + |
1011 | + // Generating .g for the environment |
1012 | + Result<? extends ExternalProcessResult> pcompResult = null; |
1013 | + File envStgFile = null; |
1014 | + if (envFile.getName().endsWith(".g")) { |
1015 | + envStgFile = envFile; |
1016 | + } else { |
1017 | + STG envStg = (STG)framework.loadFile(envFile).getMathModel(); |
1018 | + Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG); |
1019 | + envStgFile = new File(workingDirectory, "env.g"); |
1020 | + ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath()); |
1021 | + Result<? extends Object> envExportResult = framework.getTaskManager().execute( |
1022 | + envExportTask, "Exporting environment .g", subtaskMonitor); |
1023 | + |
1024 | + if (envExportResult.getOutcome() != Outcome.FINISHED) { |
1025 | + if (envExportResult.getOutcome() == Outcome.CANCELLED) { |
1026 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1027 | + } |
1028 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1029 | + new MpsatChainResult(envExportResult, null, null, null, toolchainPreparationSettings)); |
1030 | + } |
1031 | + } |
1032 | + monitor.progressUpdate(0.40); |
1033 | + |
1034 | + // Generating .g for the whole system (model and environment) |
1035 | + File stgFile = new File(workingDirectory, "system.g"); |
1036 | + PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, ConversionMode.OUTPUT, true, false, workingDirectory); |
1037 | + pcompResult = framework.getTaskManager().execute( |
1038 | + pcompTask, "Running pcomp", subtaskMonitor); |
1039 | + |
1040 | + if (pcompResult.getOutcome() != Outcome.FINISHED) { |
1041 | + if (pcompResult.getOutcome() == Outcome.CANCELLED) { |
1042 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1043 | + } |
1044 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1045 | + new MpsatChainResult(devExportResult, pcompResult, null, null, toolchainPreparationSettings)); |
1046 | + } |
1047 | + FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput())); |
1048 | + WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true); |
1049 | + STG stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel(); |
1050 | + monitor.progressUpdate(0.50); |
1051 | + |
1052 | + // Generate unfolding |
1053 | + File unfoldingFile = new File(workingDirectory, "system" + MpsatUtilitySettings.getUnfoldingExtension()); |
1054 | + PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath()); |
1055 | + Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute( |
1056 | + punfTask, "Unfolding .g", subtaskMonitor); |
1057 | + |
1058 | + if (punfResult.getOutcome() != Outcome.FINISHED) { |
1059 | + if (punfResult.getOutcome() == Outcome.CANCELLED) { |
1060 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1061 | + } |
1062 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1063 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainPreparationSettings)); |
1064 | + } |
1065 | + monitor.progressUpdate(0.60); |
1066 | + |
1067 | + // Check for interface conformation |
1068 | + Set<String> devOutputNames = devStg.getSignalFlatNames(Type.OUTPUT); |
1069 | + Set<String> devPlaceNames = parsePlaceNames(pcompResult.getReturnValue().getOutputFile("places.list"), 0); |
1070 | +// String reachConformation = MpsatSettings.genReachConformation(devOutputNames, devPlaceNames); |
1071 | + String reachConformation = MpsatSettings.genReachConformationDetail(stg, devOutputNames, devPlaceNames); |
1072 | + if (MpsatUtilitySettings.getDebugReach()) { |
1073 | + System.out.println("\nReach expression for the interface conformation property:"); |
1074 | + System.out.println(reachConformation); |
1075 | + } |
1076 | + MpsatSettings conformationSettings = new MpsatSettings("Interface conformation", |
1077 | + MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), |
1078 | + MpsatUtilitySettings.getSolutionCount(), reachConformation); |
1079 | + |
1080 | + MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), |
1081 | + unfoldingFile.getCanonicalPath(), workingDirectory); |
1082 | + Result<? extends ExternalProcessResult> mpsatConformationResult = framework.getTaskManager().execute( |
1083 | + mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor); |
1084 | + |
1085 | + if (mpsatConformationResult.getOutcome() != Outcome.FINISHED) { |
1086 | + if (mpsatConformationResult.getOutcome() == Outcome.CANCELLED) { |
1087 | + return new Result<MpsatChainResult>(Outcome.CANCELLED); |
1088 | + } |
1089 | + return new Result<MpsatChainResult>(Outcome.FAILED, |
1090 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings)); |
1091 | + } |
1092 | + monitor.progressUpdate(0.80); |
1093 | + |
1094 | + MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue()); |
1095 | + if (!mpsatConformationParser.getSolutions().isEmpty()) { |
1096 | + return new Result<MpsatChainResult>(Outcome.FINISHED, |
1097 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, |
1098 | + "This model does not conform to the environment after the following trace:")); |
1099 | + } |
1100 | + monitor.progressUpdate(1.0); |
1101 | + |
1102 | + // Success |
1103 | + unfoldingFile.delete(); |
1104 | + String message = "The model conforms to its environment (" + envFile.getName() + ")."; |
1105 | + return new Result<MpsatChainResult>(Outcome.FINISHED, |
1106 | + new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message)); |
1107 | + |
1108 | + } catch (Throwable e) { |
1109 | + return new Result<MpsatChainResult>(e); |
1110 | + } finally { |
1111 | + if ((workingDirectory != null) && !MpsatUtilitySettings.getDebugTemporaryFiles()) { |
1112 | + FileUtils.deleteDirectoryTree(workingDirectory); |
1113 | + } |
1114 | + } |
1115 | + } |
1116 | + |
1117 | + |
1118 | + private HashSet<String> parsePlaceNames(byte[] bufferedInput, int lineIndex) { |
1119 | + HashSet<String> result = new HashSet<String>(); |
1120 | + InputStream is = new ByteArrayInputStream(bufferedInput); |
1121 | + BufferedReader br = new BufferedReader(new InputStreamReader(is)); |
1122 | + try { |
1123 | + String line = null; |
1124 | + while ((lineIndex >= 0) && ((line = br.readLine()) != null)) { |
1125 | + lineIndex--; |
1126 | + } |
1127 | + if (line != null) { |
1128 | + for (String name: line.trim().split("\\s")) { |
1129 | + result.add(name); |
1130 | + } |
1131 | + } |
1132 | + } catch (IOException e) { |
1133 | + e.printStackTrace(); |
1134 | + } |
1135 | + return result; |
1136 | + } |
1137 | + |
1138 | + |
1139 | +} |
1140 | |
1141 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java' |
1142 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java 2014-11-13 00:05:09 +0000 |
1143 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java 2014-11-30 23:14:46 +0000 |
1144 | @@ -16,12 +16,21 @@ |
1145 | import org.workcraft.util.FileUtils; |
1146 | |
1147 | public class MpsatTask implements Task<ExternalProcessResult> { |
1148 | - private String[] args; |
1149 | - private String inputFileName; |
1150 | - |
1151 | + private final String[] args; |
1152 | + private final String inputFileName; |
1153 | + private final File workingDirectory; |
1154 | + |
1155 | public MpsatTask(String[] args, String inputFileName) { |
1156 | + this(args, inputFileName, null); |
1157 | + } |
1158 | + |
1159 | + public MpsatTask(String[] args, String inputFileName, File workingDirectory) { |
1160 | this.args = args; |
1161 | this.inputFileName = inputFileName; |
1162 | + if (workingDirectory == null) { |
1163 | + workingDirectory = FileUtils.createTempDirectory("mpsat_"); |
1164 | + } |
1165 | + this.workingDirectory = workingDirectory; |
1166 | } |
1167 | |
1168 | @Override |
1169 | @@ -43,23 +52,20 @@ |
1170 | // Input file argument |
1171 | command.add(inputFileName); |
1172 | |
1173 | - File workingDir = FileUtils.createTempDirectory("mpsat_"); |
1174 | - ExternalProcessTask externalProcessTask = new ExternalProcessTask(command, workingDir); |
1175 | - |
1176 | + ExternalProcessTask externalProcessTask = new ExternalProcessTask(command, workingDirectory); |
1177 | Result<? extends ExternalProcessResult> res = externalProcessTask.run(monitor); |
1178 | - |
1179 | - if(res.getOutcome() == Outcome.CANCELLED) |
1180 | + if(res.getOutcome() == Outcome.CANCELLED) { |
1181 | return res; |
1182 | + } |
1183 | |
1184 | Map<String, byte[]> outputFiles = new HashMap<String, byte[]>(); |
1185 | - |
1186 | try { |
1187 | String unfoldingFileName = "mpsat" + MpsatUtilitySettings.getUnfoldingExtension(); |
1188 | - File unfoldingFile = new File(workingDir, unfoldingFileName); |
1189 | + File unfoldingFile = new File(workingDirectory, unfoldingFileName); |
1190 | if(unfoldingFile.exists()) { |
1191 | outputFiles.put(unfoldingFileName, FileUtils.readAllBytes(unfoldingFile)); |
1192 | } |
1193 | - File g = new File(workingDir, "mpsat.g"); |
1194 | + File g = new File(workingDirectory, "mpsat.g"); |
1195 | if(g.exists()) { |
1196 | outputFiles.put("mpsat.g", FileUtils.readAllBytes(g)); |
1197 | } |
1198 | @@ -69,10 +75,11 @@ |
1199 | |
1200 | ExternalProcessResult retVal = res.getReturnValue(); |
1201 | ExternalProcessResult result = new ExternalProcessResult(retVal.getReturnCode(), retVal.getOutput(), retVal.getErrors(), outputFiles); |
1202 | - |
1203 | - if (retVal.getReturnCode() < 2) |
1204 | + if (retVal.getReturnCode() < 2) { |
1205 | return Result.finished(result); |
1206 | - else |
1207 | + } else { |
1208 | return Result.failed(result); |
1209 | + } |
1210 | } |
1211 | -} |
1212 | \ No newline at end of file |
1213 | + |
1214 | +} |
1215 | |
1216 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java' |
1217 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java 2014-06-20 21:35:25 +0000 |
1218 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java 2014-11-30 23:14:46 +0000 |
1219 | @@ -22,15 +22,19 @@ |
1220 | |
1221 | @Override |
1222 | public final void run(WorkspaceEntry we) { |
1223 | + final MpsatSettings settings = getSettings(); |
1224 | + final MpsatChainTask mpsatTask = new MpsatChainTask(we, settings, framework); |
1225 | + |
1226 | String description = "MPSat tool chain"; |
1227 | String title = we.getModelEntry().getModel().getTitle(); |
1228 | if (!title.isEmpty()) { |
1229 | description += "(" + title +")"; |
1230 | } |
1231 | - final MpsatChainTask mpsatTask = new MpsatChainTask(we, getSettings(), framework); |
1232 | - framework.getTaskManager().queue(mpsatTask, description, new MpsatChainResultHandler(mpsatTask)); |
1233 | + MpsatChainResultHandler monitor = new MpsatChainResultHandler(mpsatTask); |
1234 | + |
1235 | + framework.getTaskManager().queue(mpsatTask, description, monitor); |
1236 | } |
1237 | - |
1238 | + |
1239 | @Override |
1240 | public abstract String getDisplayName(); |
1241 | |
1242 | |
1243 | === added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java' |
1244 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java 1970-01-01 00:00:00 +0000 |
1245 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java 2014-11-30 23:14:46 +0000 |
1246 | @@ -0,0 +1,56 @@ |
1247 | +package org.workcraft.plugins.mpsat.tools; |
1248 | + |
1249 | +import java.io.File; |
1250 | + |
1251 | +import javax.swing.JFileChooser; |
1252 | + |
1253 | +import org.workcraft.Framework; |
1254 | +import org.workcraft.Tool; |
1255 | +import org.workcraft.plugins.mpsat.MpsatChainResultHandler; |
1256 | +import org.workcraft.plugins.mpsat.tasks.MpsatConformationTask; |
1257 | +import org.workcraft.plugins.stg.STGModel; |
1258 | +import org.workcraft.util.WorkspaceUtils; |
1259 | +import org.workcraft.workspace.WorkspaceEntry; |
1260 | + |
1261 | +public class MpsatConformationChecker implements Tool { |
1262 | + private final Framework framework; |
1263 | + |
1264 | + public MpsatConformationChecker(Framework framework) { |
1265 | + this.framework = framework; |
1266 | + } |
1267 | + |
1268 | + @Override |
1269 | + public String getSection() { |
1270 | + return "Verification"; |
1271 | + } |
1272 | + |
1273 | + @Override |
1274 | + public String getDisplayName() { |
1275 | + return "Check for conformation (without dummies) [MPSat]..."; |
1276 | + } |
1277 | + |
1278 | + @Override |
1279 | + public boolean isApplicableTo(WorkspaceEntry we) { |
1280 | + return WorkspaceUtils.canHas(we, STGModel.class); |
1281 | + } |
1282 | + |
1283 | + @Override |
1284 | + public final void run(WorkspaceEntry we) { |
1285 | + JFileChooser fc = framework.getMainWindow().createOpenDialog("Open environment file", false, null); |
1286 | + if (fc.showDialog(null, "Open") == JFileChooser.APPROVE_OPTION) { |
1287 | + File file = fc.getSelectedFile(); |
1288 | + if (framework.checkFile(file)) { |
1289 | + final MpsatConformationTask mpsatTask = new MpsatConformationTask(we, framework, file); |
1290 | + |
1291 | + String description = "MPSat tool chain"; |
1292 | + String title = we.getModelEntry().getModel().getTitle(); |
1293 | + if (!title.isEmpty()) { |
1294 | + description += "(" + title +")"; |
1295 | + } |
1296 | + MpsatChainResultHandler monitor = new MpsatChainResultHandler(mpsatTask); |
1297 | + |
1298 | + framework.getTaskManager().queue(mpsatTask, description, monitor); |
1299 | + } |
1300 | + } |
1301 | + } |
1302 | +} |
1303 | |
1304 | === renamed file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/CustomPropertyMpsatChecker.java' => 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatCustomPropertyChecker.java' |
1305 | --- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/CustomPropertyMpsatChecker.java 2014-04-16 21:55:15 +0000 |
1306 | +++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatCustomPropertyChecker.java 2014-11-30 23:14:46 +0000 |
1307 | @@ -15,9 +15,9 @@ |
1308 | import org.workcraft.util.WorkspaceUtils; |
1309 | import org.workcraft.workspace.WorkspaceEntry; |
1310 | |
1311 | -public class CustomPropertyMpsatChecker implements Tool { |
1312 | +public class MpsatCustomPropertyChecker implements Tool { |
1313 | |
1314 | - public CustomPropertyMpsatChecker(Framework framework) { |
1315 | + public MpsatCustomPropertyChecker(Framework framework) { |
1316 | this.framework = framework; |
1317 | } |
1318 | |
1319 | |
1320 | === removed file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java' |
1321 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java 2010-10-06 15:51:01 +0000 |
1322 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java 1970-01-01 00:00:00 +0000 |
1323 | @@ -1,7 +0,0 @@ |
1324 | -package org.workcraft.plugins.pcomp; |
1325 | - |
1326 | -public enum PCompOutputMode { |
1327 | - DUMMY, |
1328 | - INTERNAL, |
1329 | - OUTPUT |
1330 | -} |
1331 | |
1332 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java' |
1333 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java 2014-09-05 15:06:01 +0000 |
1334 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java 2014-11-30 23:14:46 +0000 |
1335 | @@ -22,7 +22,7 @@ |
1336 | import org.workcraft.gui.trees.TreeWindow; |
1337 | import org.workcraft.gui.workspace.Path; |
1338 | import org.workcraft.gui.workspace.WorkspaceChooser; |
1339 | -import org.workcraft.plugins.pcomp.PCompOutputMode; |
1340 | +import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode; |
1341 | import org.workcraft.plugins.stg.STGWorkspaceFilter; |
1342 | |
1343 | @SuppressWarnings("serial") |
1344 | @@ -62,14 +62,13 @@ |
1345 | return improvedPcomp.isSelected(); |
1346 | } |
1347 | |
1348 | - public PCompOutputMode getMode() |
1349 | - { |
1350 | + public ConversionMode getMode() { |
1351 | if (leaveOutputs.isSelected()) |
1352 | - return PCompOutputMode.OUTPUT; |
1353 | + return ConversionMode.OUTPUT; |
1354 | if (internalize.isSelected()) |
1355 | - return PCompOutputMode.INTERNAL; |
1356 | + return ConversionMode.INTERNAL; |
1357 | if (dummify.isSelected()) |
1358 | - return PCompOutputMode.DUMMY; |
1359 | + return ConversionMode.DUMMY; |
1360 | throw new NotSupportedException("No button is selected. Cannot proceed."); |
1361 | } |
1362 | |
1363 | |
1364 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java' |
1365 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java 2014-09-05 15:06:01 +0000 |
1366 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java 2014-11-30 23:14:46 +0000 |
1367 | @@ -3,28 +3,38 @@ |
1368 | import java.io.File; |
1369 | import java.io.IOException; |
1370 | import java.util.ArrayList; |
1371 | +import java.util.HashMap; |
1372 | +import java.util.Map; |
1373 | |
1374 | -import org.workcraft.plugins.pcomp.PCompOutputMode; |
1375 | import org.workcraft.plugins.pcomp.PcompUtilitySettings; |
1376 | import org.workcraft.plugins.shared.tasks.ExternalProcessResult; |
1377 | import org.workcraft.plugins.shared.tasks.ExternalProcessTask; |
1378 | import org.workcraft.tasks.ProgressMonitor; |
1379 | import org.workcraft.tasks.Result; |
1380 | +import org.workcraft.tasks.Result.Outcome; |
1381 | import org.workcraft.tasks.Task; |
1382 | -import org.workcraft.tasks.Result.Outcome; |
1383 | import org.workcraft.util.FileUtils; |
1384 | |
1385 | public class PcompTask implements Task<ExternalProcessResult> { |
1386 | - private File[] inputs; |
1387 | - private final PCompOutputMode mode; |
1388 | - private final boolean sharedOutputs; |
1389 | - private final boolean improved; |
1390 | - |
1391 | - public PcompTask(File[] inputs, PCompOutputMode mode, boolean sharedOutputs, boolean improved) { |
1392 | - this.inputs = inputs; |
1393 | - this.mode = mode; |
1394 | - this.sharedOutputs = sharedOutputs; |
1395 | - this.improved = improved; |
1396 | + |
1397 | + public enum ConversionMode { |
1398 | + DUMMY, |
1399 | + INTERNAL, |
1400 | + OUTPUT |
1401 | + } |
1402 | + |
1403 | + private final File[] inputFiles; |
1404 | + private final ConversionMode conversionMode; |
1405 | + private final boolean useSharedOutputs; |
1406 | + private final boolean useImprovedComposition; |
1407 | + private final File workingDirectory; |
1408 | + |
1409 | + public PcompTask(File[] inputFiles, ConversionMode conversionMode, boolean useSharedOutputs, boolean useImprovedComposition, File workingDirectory) { |
1410 | + this.inputFiles = inputFiles; |
1411 | + this.conversionMode = conversionMode; |
1412 | + this.useSharedOutputs = useSharedOutputs; |
1413 | + this.useImprovedComposition = useImprovedComposition; |
1414 | + this.workingDirectory = workingDirectory; |
1415 | } |
1416 | |
1417 | @Override |
1418 | @@ -38,60 +48,58 @@ |
1419 | } |
1420 | } |
1421 | |
1422 | - if (mode == PCompOutputMode.DUMMY) { |
1423 | + if (conversionMode == ConversionMode.DUMMY) { |
1424 | command.add("-d"); |
1425 | command.add("-r"); |
1426 | - } |
1427 | - |
1428 | - if (mode == PCompOutputMode.INTERNAL) { |
1429 | + } else if (conversionMode == ConversionMode.INTERNAL) { |
1430 | command.add("-i"); |
1431 | } |
1432 | |
1433 | - if (sharedOutputs) { |
1434 | + if (useSharedOutputs) { |
1435 | command.add("-o"); |
1436 | } |
1437 | |
1438 | - if (improved) { |
1439 | + if (useImprovedComposition) { |
1440 | command.add("-p"); |
1441 | } |
1442 | |
1443 | - File listFile; |
1444 | - |
1445 | + File listFile = null; |
1446 | try { |
1447 | - listFile = File.createTempFile("pcomp_", ".list"); |
1448 | + if (workingDirectory == null) { |
1449 | + listFile = File.createTempFile("places_", ".list"); |
1450 | + } else { |
1451 | + listFile = new File(workingDirectory, "places.list"); |
1452 | + } |
1453 | } catch (IOException e) { |
1454 | return Result.exception(e); |
1455 | } |
1456 | + command.add("-l" + listFile.getAbsolutePath()); |
1457 | + |
1458 | + for (File inputFile: inputFiles) { |
1459 | + command.add(inputFile.getAbsolutePath()); |
1460 | + } |
1461 | |
1462 | - try |
1463 | - { |
1464 | - StringBuilder fileList = new StringBuilder(); |
1465 | - for (File f : inputs) |
1466 | - { |
1467 | - fileList.append(f.getAbsolutePath()); |
1468 | - fileList.append('\n'); |
1469 | - } |
1470 | - |
1471 | - try { |
1472 | - FileUtils.writeAllText(listFile, fileList.toString()); |
1473 | - } catch (IOException e) { |
1474 | - return Result.exception(e); |
1475 | - } |
1476 | - |
1477 | - command.add("@"+listFile.getAbsolutePath()); |
1478 | - |
1479 | - Result<? extends ExternalProcessResult> res = new ExternalProcessTask(command, new File(".")).run(monitor); |
1480 | - if (res.getOutcome() != Outcome.FINISHED) |
1481 | - return res; |
1482 | - |
1483 | - ExternalProcessResult retVal = res.getReturnValue(); |
1484 | - if (retVal.getReturnCode() < 2) |
1485 | - return Result.finished(retVal); |
1486 | - else |
1487 | - return Result.failed(retVal); |
1488 | - } |
1489 | - finally { |
1490 | - listFile.delete(); |
1491 | - } |
1492 | + Result<? extends ExternalProcessResult> res = new ExternalProcessTask(command, new File(".")).run(monitor); |
1493 | + if (res.getOutcome() != Outcome.FINISHED) { |
1494 | + return res; |
1495 | + } |
1496 | + |
1497 | + Map<String, byte[]> outputFiles = new HashMap<String, byte[]>(); |
1498 | + try { |
1499 | + if(listFile.exists()) { |
1500 | + outputFiles.put("places.list", FileUtils.readAllBytes(listFile)); |
1501 | + } |
1502 | + } catch (IOException e) { |
1503 | + return new Result<ExternalProcessResult>(e); |
1504 | + } |
1505 | + |
1506 | + ExternalProcessResult retVal = res.getReturnValue(); |
1507 | + ExternalProcessResult result = new ExternalProcessResult(retVal.getReturnCode(), retVal.getOutput(), retVal.getErrors(), outputFiles); |
1508 | + if (retVal.getReturnCode() < 2) { |
1509 | + return Result.finished(result); |
1510 | + } else { |
1511 | + return Result.failed(result); |
1512 | + } |
1513 | + |
1514 | } |
1515 | } |
1516 | \ No newline at end of file |
1517 | |
1518 | === modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java' |
1519 | --- MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java 2014-09-05 15:06:01 +0000 |
1520 | +++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java 2014-11-30 23:14:46 +0000 |
1521 | @@ -46,7 +46,7 @@ |
1522 | } |
1523 | |
1524 | PcompTask pcompTask = new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), |
1525 | - dialog.isSharedOutputsChecked(), dialog.isImprovedPcompChecked()); |
1526 | + dialog.isSharedOutputsChecked(), dialog.isImprovedPcompChecked(), null); |
1527 | |
1528 | PcompResultHandler pcompResult = new PcompResultHandler(framework, dialog.showInEditor()); |
1529 | |
1530 | |
1531 | === modified file 'STGPlugin/src/org/workcraft/plugins/stg/STG.java' |
1532 | --- STGPlugin/src/org/workcraft/plugins/stg/STG.java 2014-11-03 18:11:53 +0000 |
1533 | +++ STGPlugin/src/org/workcraft/plugins/stg/STG.java 2014-11-30 23:14:46 +0000 |
1534 | @@ -213,6 +213,16 @@ |
1535 | } |
1536 | }); |
1537 | } |
1538 | + |
1539 | + public Set<String> getSignalFlatNames(Type type) { |
1540 | + Set<String> result = new HashSet<String>(); |
1541 | + for (SignalTransition st : getSignalTransitions(type)) { |
1542 | + String ref = getSignalReference(st); |
1543 | + String flatName = NamespaceHelper.hierarchicalToFlatName(ref); |
1544 | + result.add(flatName); |
1545 | + } |
1546 | + return result; |
1547 | + } |
1548 | |
1549 | @Override |
1550 | public Set<String> getSignalReferences(Type type) { |
1551 | @@ -359,8 +369,8 @@ |
1552 | throw new RuntimeException("An implicit place cannot have more that one transition in its preset or postset."); |
1553 | } |
1554 | |
1555 | - return "<" + NamespaceHelper.getFlatName(referenceManager.getNodeReference(null, preset.iterator().next())) |
1556 | - + "," + NamespaceHelper.getFlatName(referenceManager.getNodeReference(null, postset.iterator().next())) + ">"; |
1557 | + return "<" + NamespaceHelper.hierarchicalToFlatName(referenceManager.getNodeReference(null, preset.iterator().next())) |
1558 | + + "," + NamespaceHelper.hierarchicalToFlatName(referenceManager.getNodeReference(null, postset.iterator().next())) + ">"; |
1559 | } |
1560 | } |
1561 | return super.getNodeReference(provider, node); |
1562 | @@ -369,27 +379,27 @@ |
1563 | @Override |
1564 | public Node getNodeByReference(NamespaceProvider provider, String reference) { |
1565 | Pair<String, String> implicitPlaceTransitions = LabelParser.parseImplicitPlaceReference(reference); |
1566 | - |
1567 | if (implicitPlaceTransitions != null) { |
1568 | Node t1 = referenceManager.getNodeByReference(provider, |
1569 | NamespaceHelper.flatToHierarchicalName(implicitPlaceTransitions.getFirst()) ); |
1570 | + |
1571 | Node t2 = referenceManager.getNodeByReference(provider, |
1572 | NamespaceHelper.flatToHierarchicalName(implicitPlaceTransitions.getSecond()) ); |
1573 | - |
1574 | - Set<Node> implicitPlaceCandidates = SetUtils.intersection(getPreset(t2), getPostset(t1)); |
1575 | - |
1576 | - for (Node node : implicitPlaceCandidates) { |
1577 | - if ((node instanceof STGPlace) && ((STGPlace)node).isImplicit()) { |
1578 | - return node; |
1579 | + if ((t1 != null) && (t2 != null)) { |
1580 | + Set<Node> implicitPlaceCandidates = SetUtils.intersection(getPreset(t2), getPostset(t1)); |
1581 | + |
1582 | + for (Node node : implicitPlaceCandidates) { |
1583 | + if ((node instanceof STGPlace) && ((STGPlace)node).isImplicit()) { |
1584 | + return node; |
1585 | + } |
1586 | } |
1587 | } |
1588 | - |
1589 | throw new NotFoundException("Implicit place between " |
1590 | + implicitPlaceTransitions.getFirst() + " and " |
1591 | + implicitPlaceTransitions.getSecond() + " does not exist."); |
1592 | - } else |
1593 | - |
1594 | + } else { |
1595 | return super.getNodeByReference(provider, reference); |
1596 | + } |
1597 | } |
1598 | |
1599 | public void makeExplicit(STGPlace implicitPlace) { |
1600 | |
1601 | === modified file 'STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java' |
1602 | --- STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java 2014-07-28 13:32:42 +0000 |
1603 | +++ STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java 2014-11-30 23:14:46 +0000 |
1604 | @@ -66,7 +66,7 @@ |
1605 | |
1606 | for (String s : sortedNames) { |
1607 | out.print(" "); |
1608 | - out.print(NamespaceHelper.getFlatName(s)); |
1609 | + out.print(NamespaceHelper.hierarchicalToFlatName(s)); |
1610 | } |
1611 | |
1612 | out.print("\n"); |
1613 | @@ -90,7 +90,7 @@ |
1614 | return; |
1615 | |
1616 | if (model.getPostset(node).size()>0) { |
1617 | - out.write(NamespaceHelper.getFlatName(model.getNodeReference(node))); |
1618 | + out.write(NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(node))); |
1619 | |
1620 | for (Node n : sortNodes (model.getPostset(node), model) ) { |
1621 | if (n instanceof STGPlace) { |
1622 | @@ -98,11 +98,11 @@ |
1623 | Collection<Node> postset = model.getPostset(n); |
1624 | if (postset.size() > 1) |
1625 | throw new FormatException("Implicit place cannot have more than one node in postset"); |
1626 | - out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(postset.iterator().next()))); |
1627 | + out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(postset.iterator().next()))); |
1628 | } else |
1629 | - out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(n))); |
1630 | + out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(n))); |
1631 | } else { |
1632 | - out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(n))); |
1633 | + out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(n))); |
1634 | } |
1635 | } |
1636 | |
1637 | @@ -165,12 +165,12 @@ |
1638 | |
1639 | if (p instanceof STGPlace) { |
1640 | if ( ((STGPlace)p).isImplicit() ) { |
1641 | - reference = "<" + NamespaceHelper.getFlatName(model.getNodeReference(model.getPreset(p).iterator().next())) + "," + |
1642 | - NamespaceHelper.getFlatName(model.getNodeReference(model.getPostset(p).iterator().next())) + ">"; |
1643 | + reference = "<" + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(model.getPreset(p).iterator().next())) + "," + |
1644 | + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(model.getPostset(p).iterator().next())) + ">"; |
1645 | } else |
1646 | - reference = NamespaceHelper.getFlatName(model.getNodeReference(p)); |
1647 | + reference = NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p)); |
1648 | } else { |
1649 | - reference = NamespaceHelper.getFlatName(model.getNodeReference(p)); |
1650 | + reference = NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p)); |
1651 | } |
1652 | |
1653 | if (tokens == 1) |
1654 | @@ -201,7 +201,7 @@ |
1655 | for (Place p : places) { |
1656 | if (p instanceof STGPlace) |
1657 | if (((STGPlace)p).getCapacity() != 1) |
1658 | - capacity.append(" " + NamespaceHelper.getFlatName(model.getNodeReference(p)) + "=" + ((STGPlace)p).getCapacity()); |
1659 | + capacity.append(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p)) + "=" + ((STGPlace)p).getCapacity()); |
1660 | } |
1661 | |
1662 | if (capacity.length() > 0) |
1663 | @@ -212,7 +212,7 @@ |
1664 | LinkedList<String> transitions = new LinkedList<String>(); |
1665 | |
1666 | for (Transition t : net.getTransitions()) |
1667 | - transitions.add(NamespaceHelper.getFlatName(net.getNodeReference(t))); |
1668 | + transitions.add(NamespaceHelper.hierarchicalToFlatName(net.getNodeReference(t))); |
1669 | |
1670 | writeSignalsHeader(out, transitions, ".dummy"); |
1671 | |
1672 | |
1673 | === modified file 'Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java' |
1674 | --- Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java 2014-07-11 09:35:42 +0000 |
1675 | +++ Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java 2014-11-30 23:14:46 +0000 |
1676 | @@ -68,7 +68,7 @@ |
1677 | String hName = en.getKey(); |
1678 | String fName = en.getValue(); |
1679 | |
1680 | - String answer = NamespaceHelper.getFlatName(hName); |
1681 | + String answer = NamespaceHelper.hierarchicalToFlatName(hName); |
1682 | assertTrue(answer.equals(fName)); |
1683 | |
1684 | hName = hName.replaceAll("'", ""); |
1685 | |
1686 | === modified file 'WorkcraftCore/src/org/workcraft/Info.java' |
1687 | --- WorkcraftCore/src/org/workcraft/Info.java 2014-11-24 15:37:13 +0000 |
1688 | +++ WorkcraftCore/src/org/workcraft/Info.java 2014-11-30 23:14:46 +0000 |
1689 | @@ -13,7 +13,7 @@ |
1690 | private static final int majorVersion = 3; |
1691 | private static final int minorVersion = 0; |
1692 | private static final int revisionVersion = 3; |
1693 | - private static final String statusVersion = "alpha"; |
1694 | + private static final String statusVersion = "beta"; |
1695 | |
1696 | private static final int startYear = 2006; |
1697 | private static final int currentYear = Calendar.getInstance().get(Calendar.YEAR); |
1698 | |
1699 | === modified file 'WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java' |
1700 | --- WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java 2014-11-12 18:06:50 +0000 |
1701 | +++ WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java 2014-11-30 23:14:46 +0000 |
1702 | @@ -23,20 +23,20 @@ |
1703 | // TODO: make it work with the embedded ' characters |
1704 | private static Pattern hPattern = Pattern.compile("(/)?(((\\'([^\\']+)\\')|([_A-Za-z][_A-Za-z0-9]*))([\\+\\-\\~])?(/[0-9]+)?)(.*)"); |
1705 | |
1706 | - public static String getFlatName(String reference) { |
1707 | - return getFlatName(reference, flatNameSeparator, true); |
1708 | + public static String hierarchicalToFlatName(String reference) { |
1709 | + return hierarchicalToFlatName(reference, flatNameSeparator, true); |
1710 | } |
1711 | |
1712 | - private static String getFlatName(String reference, String flatSeparator, boolean isFirst) { |
1713 | + private static String hierarchicalToFlatName(String reference, String flatSeparator, boolean suppressLeadingSeparator) { |
1714 | if (flatSeparator==null) flatSeparator=flatNameSeparator; |
1715 | |
1716 | - // do not work with implicit places(?) |
1717 | + // Do not work with implicit places(?) |
1718 | if (reference.startsWith("<")) { |
1719 | return reference; |
1720 | } |
1721 | String ret = ""; |
1722 | - // in this version the first separator is not shown |
1723 | - if (!isFirst && reference.startsWith(hierarchySeparator)) { |
1724 | + // In this version the first separator is suppressed |
1725 | + if (!suppressLeadingSeparator && reference.startsWith(hierarchySeparator)) { |
1726 | ret=flatSeparator; |
1727 | } |
1728 | |
1729 | @@ -45,11 +45,11 @@ |
1730 | if (tail.equals("")) { |
1731 | return ret+head; |
1732 | } |
1733 | - return ret+head+getFlatName(tail, flatSeparator, false); |
1734 | + return ret + head + hierarchicalToFlatName(tail, flatSeparator, false); |
1735 | } |
1736 | |
1737 | - public static String flatToHierarchicalName(String reference) { |
1738 | - return flatToHierarchicalName(reference, flatNameSeparator); |
1739 | + public static String flatToHierarchicalName(String flatName) { |
1740 | + return flatToHierarchicalName(flatName, flatNameSeparator); |
1741 | } |
1742 | |
1743 | private static String flatToHierarchicalName(String reference, String flatSeparator) { |
1744 | |
1745 | === modified file 'WorkcraftCore/src/org/workcraft/gui/MainWindow.java' |
1746 | --- WorkcraftCore/src/org/workcraft/gui/MainWindow.java 2014-11-24 17:04:15 +0000 |
1747 | +++ WorkcraftCore/src/org/workcraft/gui/MainWindow.java 2014-11-30 23:14:46 +0000 |
1748 | @@ -833,7 +833,7 @@ |
1749 | } |
1750 | } |
1751 | |
1752 | - private JFileChooser createOpenDialog(String title, boolean multiSelection, Importer[] importers) { |
1753 | + public JFileChooser createOpenDialog(String title, boolean multiSelection, Importer[] importers) { |
1754 | JFileChooser fc = new JFileChooser(); |
1755 | fc.setDialogType(JFileChooser.OPEN_DIALOG); |
1756 | fc.setMultiSelectionEnabled(multiSelection); |
1757 | @@ -856,7 +856,7 @@ |
1758 | return fc; |
1759 | } |
1760 | |
1761 | - private JFileChooser createSaveDialog(String title, File file, Exporter exporter) { |
1762 | + public JFileChooser createSaveDialog(String title, File file, Exporter exporter) { |
1763 | JFileChooser fc = new JFileChooser(); |
1764 | fc.setDialogType(JFileChooser.SAVE_DIALOG); |
1765 | fc.setDialogTitle(title); |
1766 | |
1767 | === modified file 'WorkcraftCore/src/org/workcraft/util/FileUtils.java' |
1768 | --- WorkcraftCore/src/org/workcraft/util/FileUtils.java 2014-01-15 17:13:30 +0000 |
1769 | +++ WorkcraftCore/src/org/workcraft/util/FileUtils.java 2014-11-30 23:14:46 +0000 |
1770 | @@ -31,8 +31,6 @@ |
1771 | import java.io.InputStream; |
1772 | import java.io.InputStreamReader; |
1773 | import java.io.OutputStream; |
1774 | -import java.net.URI; |
1775 | -import java.net.URISyntaxException; |
1776 | import java.nio.channels.Channels; |
1777 | import java.nio.channels.FileChannel; |
1778 | import java.nio.channels.WritableByteChannel; |
1779 | |
1780 | === modified file 'build_distr_linux.sh' |
1781 | --- build_distr_linux.sh 2014-11-24 15:37:13 +0000 |
1782 | +++ build_distr_linux.sh 2014-11-30 23:14:46 +0000 |
1783 | @@ -1,7 +1,7 @@ |
1784 | #!/usr/bin/env bash |
1785 | |
1786 | src_dir="." |
1787 | -distr_dir="../../workcraft_3.0.3_alpha" |
1788 | +distr_dir="../../workcraft_3.0.3_beta" |
1789 | template_dir="../../distr-template-linux" |
1790 | |
1791 | ./build_distr.sh -s $src_dir -d $distr_dir -t $template_dir |
1792 | |
1793 | === modified file 'build_distr_windows.sh' |
1794 | --- build_distr_windows.sh 2014-11-24 15:37:13 +0000 |
1795 | +++ build_distr_windows.sh 2014-11-30 23:14:46 +0000 |
1796 | @@ -1,7 +1,7 @@ |
1797 | #!/usr/bin/env bash |
1798 | |
1799 | src_dir="." |
1800 | -distr_dir="../../workcraft_3.0.3_alpha" |
1801 | +distr_dir="../../workcraft_3.0.3_beta" |
1802 | template_dir="../../distr-template-windows" |
1803 | |
1804 | ./build_distr.sh -s $src_dir -d $distr_dir -t $template_dir |