|
1
17
18 package SOFA.SOFAnode.Util.DFSRChecker.backend;
19
20
21 import java.util.TreeSet  ;
22 import java.io.FileOutputStream ;
23 import java.io.IOException ;
24 import java.io.FileNotFoundException ;
25
26
27 import SOFA.SOFAnode.Util.DFSRChecker.CheckingResult;
28 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.CheckingException;
29 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.DFSRDotVis;
30 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.DFSRTraverser;
31 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.ItemAlreadyPresentException;
32 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.ItemNotPresentException;
33 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.Options;
34 import SOFA.SOFAnode.Util.DFSRChecker.node.ActionRepository;
35 import SOFA.SOFAnode.Util.DFSRChecker.node.ConsentNode;
36 import SOFA.SOFAnode.Util.DFSRChecker.node.DeterministicNode;
37 import SOFA.SOFAnode.Util.DFSRChecker.node.InvalidParameterException;
38 import SOFA.SOFAnode.Util.DFSRChecker.node.TreeNode;
39 import SOFA.SOFAnode.Util.DFSRChecker.optimizer.OptExplicit;
40 import SOFA.SOFAnode.Util.DFSRChecker.parser.Debug;
41 import SOFA.SOFAnode.Util.DFSRChecker.state.Signature;
42 import SOFA.SOFAnode.Util.DFSRChecker.visualization.DotVisualizer;
43
44
47 public class DotVisBackend implements IBackend {
48
49 public DotVisBackend(ActionRepository repository) {
50 this.repository = repository;
51 }
52
53
56 public CheckingResult perform(TreeNode[] nodes, String [] synchroops, String [] unboundops) {
57 if (nodes.length < 2) {
60 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Visualization backend: wrong number of items within the first array parameter (at least two required.\n");
61 }
62
63 if (synchroops.length != nodes.length - 1) {
64 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Visualization backend: wrong number of items within the second array parameter (1 lower than the number of components required).\n");
65 }
66
67 DotVisualizer dotviz = new DotVisualizer(repository);
68
69 for (int i = 0; i < nodes.length; ++i) {
71
72 dotviz.visualize(nodes[i], "pt_" + i + ".dt");
73
74 }
75
76
104 nodes[0] = ConsentBackend.invertProtocol(nodes[0], repository);
105
106 TreeNode result = new DeterministicNode(nodes[nodes.length - 1]);
107
108 TreeSet unbound = new TreeSet ();
109 for (int y = 0; y < unboundops.length; ++y) {
110 unbound.add(new Integer (repository.getItemIndex(unboundops[y])));
111 }
112
113 for (int j = nodes.length - 2; j > 0; --j) {
114 String [] sprov;
115 TreeSet prov = new TreeSet ();
116 sprov = synchroops[j].split(",");
117
118 for (int i = 0; i < sprov.length; ++i) {
119 int index = repository.getItemIndex(sprov[i]);
120 if (index == -1) {
121 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions - not occuring within the protocols.");
122 } else {
123 prov.add(new Integer (index));
124 }
125 }
126
127 result = new ConsentNode(new DeterministicNode(nodes[j]), result, prov, unbound, repository, false);
129
130 }
131
132 String [] sprov;
133 TreeSet prov = new TreeSet ();
134 sprov = synchroops[0].split(",");
135
136 for (int i = 0; i < sprov.length; ++i) {
137 int index = repository.getItemIndex(sprov[i]);
138 if (index == -1) {
139 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions - not occuring within the protocols.");
140 } else {
141 prov.add(new Integer (index));
142 }
143 }
144
145 ConsentNode top = new ConsentNode(new DeterministicNode(nodes[0]), result, prov, unbound, repository, false);
146
147 Debug.println("State space estimate: " + top.getWeight());
148
149 Debug.print("Optimizing the parse tree for the composition test......");
151 try {
152 if (Options.forwardcutting)
153 top = (ConsentNode) top.forwardCut(repository.getAllUsedEventIndices());
154
155 if (top != null)
156 Signature.setSize(top.getLeafCount());
157
158 if ((Options.explicit) && (top != null))
159 top = (ConsentNode) new OptExplicit(top, Options.explicitsize).perform();
160 } catch (InvalidParameterException e) {
161 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while performing optimization. Bailing out....");
162 }
163
164 Debug.println("done.");
165
166
167 if (top != null) {
168 DFSRTraverser dfsr1 = new DFSRTraverser(top, repository);
169
170 try {
171 FileOutputStream outputfile = new FileOutputStream ("a_main.dt");
172
173 outputfile.write("digraph G {\n size = \"7,11\";\n".getBytes());
174 dfsr1.run(new DFSRDotVis(outputfile, top, repository));
175 outputfile.write(("\n}").getBytes());
176
177 outputfile.close();
178 } catch (CheckingException e) {
179 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "End of checking while vizualizating, need a fix! - " + e.getMessage());
180 } catch (InvalidParameterException e) {
181 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (Invalid parameter exception): " + e.getMessage());
182 } catch (ItemAlreadyPresentException e) {
183 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemAlreadyPresentException): " + e.getMessage());
184 } catch (ItemNotPresentException e) {
185 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemNotPresentException): " + e.getMessage());
186 } catch (FileNotFoundException e) {
187 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Couldn't open file automaton1.dt");
188 } catch (IOException e) {
189 return new CheckingResult(CheckingResult.ERR_OTHERERROR, "IOException while writing to the file a_main.dt");
190 }
191 }
192
193 return null;
194 }
195
196
200 private ActionRepository repository;
201
202
203
204
205
206
207 } |
Popular Tags |
Java API By Example, From Geeks To Geeks.