← Back to branch summary

~danilovesky/workcraft/trunk-bug-1317910

« back to all changes in this revision

Viewing changes to PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java

  • Committer: Danil Sokolov
  • Date: 2014-04-29 16:33:54 UTC
  • mfrom: (500.1.3 trunk-circuit-env-stg)
  • Revision ID: danilovesky@gmail.com-20140429163354-roh1ya2qvu1z2p5l
Merge of blueprint circuit-env-stg to support verification of circuits under their environment STGs (conformation, deadlocks and hazards).

Show diffs side-by-side

added added

removed removed

Lines of Context:
PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java
53
53
                        File netFile = File.createTempFile("net", exporter.getExtenstion());
54
54
                        ExportTask exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath());
55
55
                        SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor);
56
 
                        Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon);
 
56
                        Result<? extends Object> exportResult = framework.getTaskManager().execute(
 
57
                                        exportTask, "Exporting .g", mon);
 
58
                        
57
59
                        if (exportResult.getOutcome() != Outcome.FINISHED) {
58
60
                                netFile.delete();
59
61
                                if (exportResult.getOutcome() == Outcome.CANCELLED) {
60
62
                                        return new Result<MpsatChainResult>(Outcome.CANCELLED);
61
63
                                }
62
64
                                return new Result<MpsatChainResult>(Outcome.FAILED, 
63
 
                                                new MpsatChainResult(exportResult, null, null, settings));
 
65
                                                new MpsatChainResult(exportResult, null, null, null, settings));
64
66
                        }
65
67
                        monitor.progressUpdate(0.20);
66
68
                        
67
69
                        File mciFile = File.createTempFile("unfolding", ".mci");
68
70
                        PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
69
 
                        Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
 
71
                        Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 
72
                                        punfTask, "Unfolding .g", mon);
 
73
                        
70
74
                        netFile.delete();
71
75
                        if (punfResult.getOutcome() != Outcome.FINISHED) {
72
76
                                mciFile.delete();
74
78
                                        return new Result<MpsatChainResult>(Outcome.CANCELLED);
75
79
                                }
76
80
                                return new Result<MpsatChainResult>(Outcome.FAILED, 
77
 
                                                new MpsatChainResult(exportResult, punfResult, null, settings));
 
81
                                                new MpsatChainResult(exportResult, null, punfResult, null, settings));
78
82
                        }
79
83
                        monitor.progressUpdate(0.70);
80
84
 
81
85
                        MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
82
 
                        Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
 
86
                        Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 
87
                                        mpsatTask, "Running deadlock checking [MPSat]", mon);
 
88
                        
83
89
                        if (mpsatResult.getOutcome() != Outcome.FINISHED) {
84
90
                                if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
85
91
                                        return new Result<MpsatChainResult>(Outcome.CANCELLED);
86
92
                                }
87
93
                                return new Result<MpsatChainResult>(Outcome.FAILED, 
88
 
                                                new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, new String(mpsatResult.getReturnValue().getErrors())));
 
94
                                                new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, 
 
95
                                                                new String(mpsatResult.getReturnValue().getErrors())));
89
96
                        }
90
97
                        monitor.progressUpdate(0.90);
91
98
                        
93
100
                        if (!mdp.getSolutions().isEmpty()) {
94
101
                                mciFile.delete();
95
102
                                return new Result<MpsatChainResult>(Outcome.FINISHED, 
96
 
                                                new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net has a deadlock"));
 
103
                                                new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net has a deadlock"));
97
104
                        }
98
105
                        monitor.progressUpdate(1.0);
99
106
 
100
107
                        mciFile.delete();
101
108
                        return new Result<MpsatChainResult>(Outcome.FINISHED, 
102
 
                                        new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net is deadlock-free"));
 
109
                                        new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net is deadlock-free"));
103
110
                        
104
111
                } catch (Throwable e) {
105
112
                        return new Result<MpsatChainResult>(e);