00001 package edu.ksu.cis.bandera.abstraction.gui;
00002
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004 * Bandera, a Java(TM) analysis and transformation toolkit *
00005 * Copyright (C) 2000 Robby (robby@cis.ksu.edu) *
00006 * All rights reserved. *
00007 * *
00008 * This work was done as a project in the SAnToS Laboratory, *
00009 * Department of Computing and Information Sciences, Kansas State *
00010 * University, USA (http://www.cis.ksu.edu/santos). *
00011 * It is understood that any modification not identified as such is *
00012 * not covered by the preceding statement. *
00013 * *
00014 * This work is free software; you can redistribute it and/or *
00015 * modify it under the terms of the GNU Library General Public *
00016 * License as published by the Free Software Foundation; either *
00017 * version 2 of the License, or (at your option) any later version. *
00018 * *
00019 * This work is distributed in the hope that it will be useful, *
00020 * but WITHOUT ANY WARRANTY; without even the implied warranty of *
00021 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *
00022 * Library General Public License for more details. *
00023 * *
00024 * You should have received a copy of the GNU Library General Public *
00025 * License along with this toolkit; if not, write to the *
00026 * Free Software Foundation, Inc., 59 Temple Place - Suite 330, *
00027 * Boston, MA 02111-1307, USA. *
00028 * *
00029 * Java is a trademark of Sun Microsystems, Inc. *
00030 * *
00031 * To submit a bug report, send a comment, or get the latest news on *
00032 * this project and other SAnToS projects, please visit the web-site *
00033 * http://www.cis.ksu.edu/santos *
00034 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00035 import Bandera;
00036 import java.io.*;
00037 import java.util.*;
00038 import javax.swing.*;
00039 import javax.swing.table.*;
00040 import edu.ksu.cis.bandera.bui.*;
00041 import edu.ksu.cis.bandera.abstraction.*;
00042 import edu.ksu.cis.bandera.abstraction.pvs.*;
00043 import edu.ksu.cis.bandera.abstraction.util.*;
00044 import edu.ksu.cis.bandera.abstraction.lib.integral.*;
00045 import edu.ksu.cis.bandera.abstraction.specification.*;
00046 import edu.ksu.cis.bandera.util.*;
00047 public class AbstractionLibraryManager extends JDialog {
00048 private static final Object[] columnNames = new String[] {"Name", "Tokens", "Type"};
00049 private static TreeSet abstractions = new TreeSet();
00050 public static String abstractionPackage;
00051 public static String abstractionPath;
00052 private static String abstractionListPath;
00053 static {
00054 init();
00055 }
00056 private JPanel ivjJDialogContentPane = null;
00057 private JButton ivjAddToLibraryButton = null;
00058 private JScrollPane ivjBASLCodeScrollPane = null;
00059 private JTextArea ivjBASLCodeTextArea = null;
00060 private JLabel ivjBASLLabel = null;
00061 private JScrollPane ivjLibraryScrollPane = null;
00062 private JButton ivjNewButton = null;
00063 private JButton ivjOpenButton = null;
00064 private JButton ivjPVSButton = null;
00065 private JLabel ivjPVSLogoLabel = null;
00066 private JButton ivjRemoveButton = null;
00067 private JButton ivjSaveAsButton = null;
00068 private JTable ivjScrollPaneTable = null;
00069 private JButton ivjShowButton = null;
00070 private JLabel ivjAbstractionsLabel = null;
00071 IvjEventHandler ivjEventHandler = new IvjEventHandler();
00072 class IvjEventHandler implements java.awt.event.ActionListener {
00073 public void actionPerformed(java.awt.event.ActionEvent e) {
00074 if (e.getSource() == AbstractionLibraryManager.this.getNewButton())
00075 connEtoM1(e);
00076 if (e.getSource() == AbstractionLibraryManager.this.getAddToLibraryButton())
00077 connEtoC1();
00078 if (e.getSource() == AbstractionLibraryManager.this.getPVSButton())
00079 connEtoC2();
00080 if (e.getSource() == AbstractionLibraryManager.this.getSaveAsButton())
00081 connEtoC3();
00082 if (e.getSource() == AbstractionLibraryManager.this.getOpenButton())
00083 connEtoC4();
00084 if (e.getSource() == AbstractionLibraryManager.this.getShowButton())
00085 connEtoC5();
00086 if (e.getSource() == AbstractionLibraryManager.this.getRemoveButton())
00087 connEtoC6();
00088 };
00089 };
00090 /**
00091 * AbtractionLibraryManager constructor comment.
00092 */
00093 public AbstractionLibraryManager() {
00094 super();
00095 initialize();
00096 }
00097 /**
00098 * AbtractionLibraryManager constructor comment.
00099 * @param owner java.awt.Dialog
00100 */
00101 public AbstractionLibraryManager(java.awt.Dialog owner) {
00102 super(owner);
00103 }
00104 /**
00105 * AbtractionLibraryManager constructor comment.
00106 * @param owner java.awt.Dialog
00107 * @param title java.lang.String
00108 */
00109 public AbstractionLibraryManager(java.awt.Dialog owner, String title) {
00110 super(owner, title);
00111 }
00112 /**
00113 * AbtractionLibraryManager constructor comment.
00114 * @param owner java.awt.Dialog
00115 * @param title java.lang.String
00116 * @param modal boolean
00117 */
00118 public AbstractionLibraryManager(java.awt.Dialog owner, String title, boolean modal) {
00119 super(owner, title, modal);
00120 }
00121 /**
00122 * AbtractionLibraryManager constructor comment.
00123 * @param owner java.awt.Dialog
00124 * @param modal boolean
00125 */
00126 public AbstractionLibraryManager(java.awt.Dialog owner, boolean modal) {
00127 super(owner, modal);
00128 }
00129 /**
00130 * AbtractionLibraryManager constructor comment.
00131 * @param owner java.awt.Frame
00132 */
00133 public AbstractionLibraryManager(java.awt.Frame owner) {
00134 super(owner);
00135 }
00136 /**
00137 * AbtractionLibraryManager constructor comment.
00138 * @param owner java.awt.Frame
00139 * @param title java.lang.String
00140 */
00141 public AbstractionLibraryManager(java.awt.Frame owner, String title) {
00142 super(owner, title);
00143 }
00144 /**
00145 * AbtractionLibraryManager constructor comment.
00146 * @param owner java.awt.Frame
00147 * @param title java.lang.String
00148 * @param modal boolean
00149 */
00150 public AbstractionLibraryManager(java.awt.Frame owner, String title, boolean modal) {
00151 super(owner, title, modal);
00152 }
00153 /**
00154 * AbtractionLibraryManager constructor comment.
00155 * @param owner java.awt.Frame
00156 * @param modal boolean
00157 */
00158 public AbstractionLibraryManager(java.awt.Frame owner, boolean modal) {
00159 super(owner, modal);
00160 }
00161 /**
00162 * Comment
00163 */
00164 public void addToLibraryButton_ActionEvents() {
00165 try {
00166 AbstractionGenerator ag = new AbstractionGenerator(new StringReader(getBASLCodeTextArea().getText()));
00167 String result = ag.generate(abstractionPackage);
00168 if (ag.getErrors().size() > 0) {
00169 StringBuffer buffer = new StringBuffer("Errors:\n");
00170 for (Iterator i = ag.getErrors().iterator(); i.hasNext();) {
00171 buffer.append("- " + i.next() + "\n");
00172 }
00173 if (ag.getWarnings().size() > 0) {
00174 buffer.append("Warnings:\n");
00175 for (Iterator i = ag.getWarnings().iterator(); i.hasNext();) {
00176 buffer.append("- " + i.next() + "\n");
00177 }
00178 }
00179 JOptionPane.showMessageDialog(this, buffer.toString(), "Cannnot generate abstraction", JOptionPane.ERROR_MESSAGE);
00180 } else {
00181 if (ag.getWarnings().size() > 0) {
00182 StringBuffer buffer = new StringBuffer();
00183 for (Iterator i = ag.getWarnings().iterator(); i.hasNext();) {
00184 buffer.append(i.next() + "\n");
00185 }
00186 JOptionPane.showMessageDialog(this, buffer.toString(), "Warnings", JOptionPane.INFORMATION_MESSAGE);
00187 }
00188 String filename = abstractionPath + File.separator + ag.getAbstractionType() + File.separator + ag.getAbstractionName();
00189 new File(filename + ".java").delete();
00190 new File(filename + ".class").delete();
00191 filename += ".java";
00192 PrintWriter pw = new PrintWriter(new FileWriter(filename));
00193 pw.write(result);
00194 pw.flush();
00195 pw.close();
00196 runJavac(System.getProperty("java.class.path"), filename);
00197 try {
00198 abstractions.add(AbstractionClassLoader.getClass(ag.getAbstractionFullyQualifiedName()).getName());
00199 updateAbstractionList();
00200 } catch (Exception e2) {
00201 e2.printStackTrace();
00202 JOptionPane.showMessageDialog(this, e2.getMessage(), "Abstraction installation failed", JOptionPane.ERROR_MESSAGE);
00203 }
00204 }
00205 } catch (Exception e) {
00206 e.printStackTrace();
00207 JOptionPane.showMessageDialog(this, e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
00208 }
00209 }
00210 /**
00211 * connEtoC1: (AddToLibraryButton.action. --> AbtractionLibraryManager.addToLibraryButton_ActionEvents()V)
00212 */
00213 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00214 private void connEtoC1() {
00215 try {
00216 // user code begin {1}
00217 // user code end
00218 this.addToLibraryButton_ActionEvents();
00219 // user code begin {2}
00220 // user code end
00221 } catch (java.lang.Throwable ivjExc) {
00222 // user code begin {3}
00223 // user code end
00224 handleException(ivjExc);
00225 }
00226 }
00227 /**
00228 * connEtoC2: (PVSButton.action. --> AbtractionLibraryManager.pVSButton_ActionEvents()V)
00229 */
00230 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00231 private void connEtoC2() {
00232 try {
00233 // user code begin {1}
00234 // user code end
00235 this.pVSButton_ActionEvents();
00236 // user code begin {2}
00237 // user code end
00238 } catch (java.lang.Throwable ivjExc) {
00239 // user code begin {3}
00240 // user code end
00241 handleException(ivjExc);
00242 }
00243 }
00244 /**
00245 * connEtoC3: (SaveAsButton.action. --> AbtractionLibraryManager.saveAsButton_ActionEvents()V)
00246 */
00247 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00248 private void connEtoC3() {
00249 try {
00250 // user code begin {1}
00251 // user code end
00252 this.saveAsButton_ActionEvents();
00253 // user code begin {2}
00254 // user code end
00255 } catch (java.lang.Throwable ivjExc) {
00256 // user code begin {3}
00257 // user code end
00258 handleException(ivjExc);
00259 }
00260 }
00261 /**
00262 * connEtoC4: (OpenButton.action. --> AbtractionLibraryManager.openButton_ActionEvents()V)
00263 */
00264 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00265 private void connEtoC4() {
00266 try {
00267 // user code begin {1}
00268 // user code end
00269 this.openButton_ActionEvents();
00270 // user code begin {2}
00271 // user code end
00272 } catch (java.lang.Throwable ivjExc) {
00273 // user code begin {3}
00274 // user code end
00275 handleException(ivjExc);
00276 }
00277 }
00278 /**
00279 * connEtoC5: (ShowButton.action. --> AbtractionLibraryManager.showButton_ActionEvents()V)
00280 */
00281 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00282 private void connEtoC5() {
00283 try {
00284 // user code begin {1}
00285 // user code end
00286 this.showButton_ActionEvents();
00287 // user code begin {2}
00288 // user code end
00289 } catch (java.lang.Throwable ivjExc) {
00290 // user code begin {3}
00291 // user code end
00292 handleException(ivjExc);
00293 }
00294 }
00295 /**
00296 * connEtoC6: (RemoveButton.action. --> AbtractionLibraryManager.removeButton_ActionEvents()V)
00297 */
00298 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00299 private void connEtoC6() {
00300 try {
00301 // user code begin {1}
00302 // user code end
00303 this.removeButton_ActionEvents();
00304 // user code begin {2}
00305 // user code end
00306 } catch (java.lang.Throwable ivjExc) {
00307 // user code begin {3}
00308 // user code end
00309 handleException(ivjExc);
00310 }
00311 }
00312 /**
00313 * connEtoM1: (NewButton.action.actionPerformed(java.awt.event.ActionEvent) --> BASLCodeTextArea.setText(Ljava.lang.String;)V)
00314 * @param arg1 java.awt.event.ActionEvent
00315 */
00316 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00317 private void connEtoM1(java.awt.event.ActionEvent arg1) {
00318 try {
00319 // user code begin {1}
00320 // user code end
00321 getBASLCodeTextArea().setText(new java.lang.String());
00322 // user code begin {2}
00323 // user code end
00324 } catch (java.lang.Throwable ivjExc) {
00325 // user code begin {3}
00326 // user code end
00327 handleException(ivjExc);
00328 }
00329 }
00330 /**
00331 *
00332 * @return java.util.Set
00333 */
00334 public static java.util.Set getAbstractions() {
00335 Set set = new HashSet(abstractions);
00336 set.add(Signs.class.getName());
00337 set.add(Point.class.getName());
00338 set.add(Set0.class.getName());
00339 set.add(Range01.class.getName());
00340 set.add(Range02.class.getName());
00341 set.add(Range03.class.getName());
00342 set.add(Range04.class.getName());
00343 set.add(edu.ksu.cis.bandera.abstraction.lib.real.Signs.class.getName());
00344 set.add(edu.ksu.cis.bandera.abstraction.lib.real.Point.class.getName());
00345 return set;
00346 }
00347 /**
00348 * Return the AbstractionsLabel property value.
00349 * @return javax.swing.JLabel
00350 */
00351 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00352 private javax.swing.JLabel getAbstractionsLabel() {
00353 if (ivjAbstractionsLabel == null) {
00354 try {
00355 ivjAbstractionsLabel = new javax.swing.JLabel();
00356 ivjAbstractionsLabel.setName("AbstractionsLabel");
00357 ivjAbstractionsLabel.setText("Abstractions:");
00358 ivjAbstractionsLabel.setForeground(java.awt.Color.black);
00359 // user code begin {1}
00360 // user code end
00361 } catch (java.lang.Throwable ivjExc) {
00362 // user code begin {2}
00363 // user code end
00364 handleException(ivjExc);
00365 }
00366 }
00367 return ivjAbstractionsLabel;
00368 }
00369 /**
00370 * Return the JButton2 property value.
00371 * @return javax.swing.JButton
00372 */
00373 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00374 private javax.swing.JButton getAddToLibraryButton() {
00375 if (ivjAddToLibraryButton == null) {
00376 try {
00377 ivjAddToLibraryButton = new javax.swing.JButton();
00378 ivjAddToLibraryButton.setName("AddToLibraryButton");
00379 ivjAddToLibraryButton.setMnemonic('a');
00380 ivjAddToLibraryButton.setText("Add");
00381 ivjAddToLibraryButton.setBackground(new java.awt.Color(204,204,255));
00382 // user code begin {1}
00383 // user code end
00384 } catch (java.lang.Throwable ivjExc) {
00385 // user code begin {2}
00386 // user code end
00387 handleException(ivjExc);
00388 }
00389 }
00390 return ivjAddToLibraryButton;
00391 }
00392 /**
00393 * Return the JScrollPane1 property value.
00394 * @return javax.swing.JScrollPane
00395 */
00396 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00397 private javax.swing.JScrollPane getBASLCodeScrollPane() {
00398 if (ivjBASLCodeScrollPane == null) {
00399 try {
00400 ivjBASLCodeScrollPane = new javax.swing.JScrollPane();
00401 ivjBASLCodeScrollPane.setName("BASLCodeScrollPane");
00402 ivjBASLCodeScrollPane.setBorder(BorderFactory.createLoweredBevelBorder());
00403 getBASLCodeScrollPane().setViewportView(getBASLCodeTextArea());
00404 // user code begin {1}
00405 // user code end
00406 } catch (java.lang.Throwable ivjExc) {
00407 // user code begin {2}
00408 // user code end
00409 handleException(ivjExc);
00410 }
00411 }
00412 return ivjBASLCodeScrollPane;
00413 }
00414 /**
00415 * Return the JTextArea1 property value.
00416 * @return javax.swing.JTextArea
00417 */
00418 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00419 private javax.swing.JTextArea getBASLCodeTextArea() {
00420 if (ivjBASLCodeTextArea == null) {
00421 try {
00422 ivjBASLCodeTextArea = new javax.swing.JTextArea();
00423 ivjBASLCodeTextArea.setName("BASLCodeTextArea");
00424 ivjBASLCodeTextArea.setFont(new java.awt.Font("monospaced", 0, 12));
00425 ivjBASLCodeTextArea.setBounds(0, 0, 157, 117);
00426 ivjBASLCodeTextArea.setFocusAccelerator('b');
00427 // user code begin {1}
00428 // user code end
00429 } catch (java.lang.Throwable ivjExc) {
00430 // user code begin {2}
00431 // user code end
00432 handleException(ivjExc);
00433 }
00434 }
00435 return ivjBASLCodeTextArea;
00436 }
00437 /**
00438 * Return the BASLLabel property value.
00439 * @return javax.swing.JLabel
00440 */
00441 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00442 private javax.swing.JLabel getBASLLabel() {
00443 if (ivjBASLLabel == null) {
00444 try {
00445 ivjBASLLabel = new javax.swing.JLabel();
00446 ivjBASLLabel.setName("BASLLabel");
00447 ivjBASLLabel.setDisplayedMnemonic('b');
00448 ivjBASLLabel.setText("BASL Code:");
00449 ivjBASLLabel.setForeground(java.awt.Color.black);
00450 // user code begin {1}
00451 // user code end
00452 } catch (java.lang.Throwable ivjExc) {
00453 // user code begin {2}
00454 // user code end
00455 handleException(ivjExc);
00456 }
00457 }
00458 return ivjBASLLabel;
00459 }
00460 /**
00461 *
00462 */
00463 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00464 private static void getBuilderData() {
00465 /*V1.1
00466 **start of data**
00467 D0CB838494G88G88G0ED1CCA9GGGGGGGGGGGG8CGGGE2F5E9ECE4E5F2A0E4E1F4E14DFD8DD81457153F5D1A46BCEB3BA60B8DE9CCEA3A7CD33B65E9CD7F26F59336359B730FE9ED57D4B6A58DCDCC0311CDB0A55134A4A11B4B57004817020802BAA0A2888E9F62C791A38898B0888808E0686A403C4048B0B34E3C23181A66FF6E3D6F39734E4CBBFCE41B67D91E67784E7B3B771CFB6E3D671EFB6E470CA4E75F622438789CC262120872F7BC0E106689C2CE365D5D00D874AF74C47DD788
00468 340D84F6A75217DF6A49E0DDA149A27135A9701A836FE3C78A49CE781CCD12EBDBA58AEA172307347716DFFAF66AF236A6E1B9496C7DE1C39ABCB30072G2B871A8714C5FEEC48D3702B701E21FC269497CFC87D3F53BCDB4A72D478EAA5DF96249583D52D21F91EB394A869F381DB849485C456703CF9705C42343B5EF9C2499712321018EA666A52E9D9AA79C8138A6FA265C9C8050EB6C48209B69F03E7FD577868871249E598F73A8C43E627E148E8B5C98E23E148E52E2BEB9C129D46E159EC33361B079CC6
00469 472D73C62BF1D4F29012768C553737AC0549A2A4946487B2ECF599ED23AE78BC86B46799547975737558C69B3FC574AFFC552F4E614FA83A7E4A2DF37B870F24AE7D95159FDF192670B5407BA4902F4F3E1BCDD35547B864443A98C6F95D1CFEAA476BF62E926B3679D7D8B7FB91AD3BE22D1EB4838D2EC57C78FE0A4B70BE9FA8E8AD5679F727314E163107C9C465BD3ACCBFF58ED94B6B9A3156DD67658FF7A66FE2F6F72F0E5A0EBE944A856A873A8D3488A884A81F59FBF752A1F8C20FB559A6A6EC56C63B7D
00470 0C4564B8EFB3C996784C7AD2413A25E11B43C4941B9EA82B505087A9B4D46F03713ADDA2E8030171771349FD8FB03B722EDB7308C3972948088DF5576D6AFF50F68BBAC45B2DGBED33EBD54B6987EB84303D4B86F7BDFB15B226F1110967AAC36F3C0A96A12F64F5DE45168273AE48DDD3A1E3ACF376257DC0730DF3BF561EDFCBD0536F1E2181E6801CEGF58159019604E19BAFCABAB2DD9B37D9E549E1B5DAFADCC3F623C3BE63B2DB407E1436CE291C2A2D350873654E1A0F374B12A36ABE0AF96CCB1A6DE2
00471 8F792AAEB80C37474AB0F73B7032BB7D169D9166EB9B99228FA358D8098963FD18A07057991E721C9B67FDFB036174BD8F52EE83A936404656BAA5FF261073F306277C460DF3B92798CE5F2BA0AD980877EFE6AA752D254F4398829A841201820016822DFC9E7BF8C3D2658C47D1172AFFB96FE2DDAEBC25C9F0ACEDD627EC348ECBFDC60759B8E4111CC449739D562EC39EFC5FE363FB984A78D032023722CE89249BA7A4B0A6A74F73A35DB61A47A13154DE73048485CC58894A7D09AE9B1E9623D33EE8B799E5
00472 491D0327BF2523B6F143588792C1GFC4E89E7BE0D79708828BF8947362A5FCA31FEF83707E33B1CC95E8E4F0F4038A5CBDDDD3319F9CE701AE8237FFC085A5ADC489F85547FDBE8D7202C97744482348A2874C5BDD98214338E64822D812AF889665017449C510F769A337EFE326A07FF5534D7CA11AFA9F67ABBEFFB7DA953239470D620B120F9C0CB00D681C582253C8C3AG35820D814D83DA82346AE51C67434A56294A1A7712271D533A51A72DA72D073FB1C86B4A66F8258D347250761A6918DE23AA2B42
00473 CB27253F5516036D1E2321A72FEB76A1F5DD77E86421CF6A5BF7CE21DB36725C8A146EA7CF428C6BC9E9176AF33ED75A96BFBC192CBE046C70A38FECB40D7A06C868674488083BA25036BFCD5693B6664F981D920E72CE878CD0496436F41E771394DA0EF4C3324A4D12DD026842AABB95B9DFCA213AA963FF44C6F0EC5E49F0BA9FB441GF58A7C2BA95BB88EB2545E84539732F423ACBB4CC3AED96A11E459EC9DF573BF40F4F1FACCB5CE252E4169342E75D047DEA01328EB49965AD7B80E5BED36F1173D17FA
00474 A8459F0C3038E79272AF08407170EA910D031709774D6C5D1DFE3B28FF067DCAE54C5486BC6DF4610C4B180D1DF91671537DF40E40F9A9C94137286C1A67FB06658B033A1075B03E003A00A60196832DDA0F6D52345FBE0D3C596AB9733A8C31327D151B7985154DEDECD72A7FB122CF559EA3A5295AE324A2F56AB1D01B2AB586F85A49D4DAF75BCD2BEACCB52452F9EC58E635CAECE08B96E59D71FAAF2D0759EA16AF19CD23125CE37E84560AF92F5031F1A71BAB2321FF93DF41B96B66FE1C33CCFDDFA7D51F
00475 DAB56360855B6E558D3E42ED5F2EBC691C45F5EA5CCA472AE411A620211AECAE2B4C718F59BC2C604E8406FD306FB2BC75259D524DB3AED936D9AB14D58DFFF4C90E911BE3C2B215DEB35E00E54FCD59407A41504812DB6867B27D61439F684FB47634B7C148518BFD5188E1C5058C9F4A2A384DC03CD1745F2C1CC6132957262C10BC8BE4D27CAD91AB0CBEFCD7D4AAB8CB4B7A4A2A312C3BAC6D2C2C2E3E1E5994E1476CBE12EB385CE7F33B195C9E638D2951B99B51CE95070F74A328F7451FBB187CCE307159
00476 C837097CBE32EBD1F65391AE3BE74CF6F3D61A0B7CBE320F226CD5753CDD3A25895B8DE9B6529DAA8E9F7947D07ED3D50EAF48C61D12CCBF1736B3CE0B51BAEA68814FE09DBD89658B5BDD5BFBE5E6366BE78BE0E6462B58586479A9ED57DF91D398AF41FA988F76CCE73F7E44CFE340DC7E710FBA2736DFFF5227B4E045CF59BA2736DF3F1ACFE540DC76F714F61942FE7DC91F4600F96C74E28675478B40CF8781053C02315393DBE9BA46CECA0058E433D878D482E9B99B68BC717E219C156F8FFD056F95E608
00477 7472F2F57A60861E3E841EBCBDD8B3BDC4249F2E50CADFA3523F27199EA152AB8FEB25470874251A69E91118DEED183AFEFFB6E8716B857F8B1A6935A27DCA25D6FA2BC8DF2719BEA8520DD5DA69F6117EBB4D743911584FCB5332E8CCA1DDF7C93004274171C752ADDC0727ED77CA6BB3DADC6E757DCF52E80CE5D145559C7FC13A769C3FBC1D465263C2FEC83A0E50F5BA1749E31225C6AA536EB0CF00A553050232277CE925FACFB99074277B4FAB60999A097B22670BE99EFF8EBD78BF291C14E25CF70E823E
00478 C4400A01CCC0F37F13772B7CAA5B5B9579E2A89FE0D52F72B21BDFD5673B63G66DB816FE12AFCB19E797ED40279742F694909575C797ADFD3675BA8724D81BCD015EF39C73E078EE23EF50047287265C52973DDAC45FC8D0077C73973CDAA7996C751FC8F0A7D6DCA01BD4A305FC3C07DF4A26E331D4FD26F478FBE73D54D9810D204A2BFA64A9D83F21F1313C56566ED047544C63443E3996A35DA2353E99BB6336D9FA5FDFD06BABE64582B9929709CB1BB1CF29B845E13E8175199D4D73ABF24400AFDF4FD28
00479 352759E2B24BB687AE051BEEB29F59A40266BE33F4D3297BB7EA547B7A37876D3A2DFE6ADE3F1157F9F0233B6EA7BEF8A4156B715D72D3B3552357C6E302D698E2DE9A613944D0B9765BA2A80BE3AF8BACD4E0268A4452DEC7EC3D401A85B6F298315B825BA030E5828BB0A096A5309D629C21787708FDDDE003825BD905D80040828536DAE03B2A91CB0C46B15EFD1D5A90BB7B20F1512441F993C2223A3AF34DE62345B6AA5AE583AB1776DBFDB41EDDFC23061DDD407BFC20A0A03E0FDADD1C2658C888E01B23
00480 51F7BED527761D95EF68C9AF50A4901F1B830BE97CB27BF88F670E5A86357C79A0F799D0589BD8572FF595B07F6BBF8ED44EDEF29B9499414D8F10B50FFEC3736CA56B057BF4D1EFA8F3571BEE3BECDF7BFA5CD5A05E96EF09369804BC81EF0AF97612D6DB2CFE935BE270C0323BAD947D1F7B2808E253861868DBC8173A9E7D073E2CD90F55665B3AF50A7EA91B5C75188FF5D8AC6A713D83D80FDE48B3FF9356639E4DFA2C5C04EDDEF80A5A175F0815605E7BD0894A8F835E2C4DA83F2DDECBFE6BE614EF5331
00481 BE1DA2E46572F38F0AFEG5EGA17F23131A7DA06467105D70749F34227EBF93725781EF5EDBA81F64EB496FFA8B656FCF22727D872EA87F2F25A85F843C0B047CB6CD7DC3057C1D8534FD268ADD15B3399A0FF9683D6F7A1D07A25F62B6927B1677BC543A1D4DC3FF50130ABF60BCB41EC977E0F09E6A860F8B834EC20F57157D1EACEA6F9043A86FFB32E839AC06A13877FAC7B62DE383489C8412016683850BB2023226BDDBEB191C62ECED34FCB6E7E42B7F00FBF4113362DBA7784C9533615BAC78DE1D95DF
00482 4A9F11EF7C70EC788A84DF542C782A845FFD065970B58B3E5D33BA2B6C97FC774F0A4FA2788A2AE643B7C770BDB0AB3EG413737FAB6FCCB5C7D406A9772C73DE63EB58A9E21BCE37E08671F99C7284FC80B71BEC74DE3F8C10C77B96A629ABCC72D003485B1D87E71E2EF3DB747F86A12753667BB67EB7161B3F83D57FA71F11F155963A7A6618E0C603D184EA36AB5CC7B5B7C5C418E4F39EFE34C73DFF59837ACFA9BFD62AFBE4D57160FFBC50A7C6CF8357C503739EFA56F006FFD87650FB724A8752DF8874F
00483 C01F4F21BE57846FF300820116810581ED864AFB977D561BD9A749F4FE0B872D5CE5B7F96FBCAB6D7C6E676C1FAD87266B1F936FFA72A9F16EA5EC532EF7314E5D39344E7360BD88A884A88CA896A8AF96564831D86726EDDA313AD61DFD83F577999757FF190F7EB32B773FCDDB6F41D82DFABFAD6AAD47625898AB79FCBA5C70617356A1D8D307B9752843CA21C341414F2743A19FBEEF9DE2B5F5783B1328C34EFB28431A4F29438B536A507E1E168E4773D1871350E1EE696753619E9FBEEF9D96E96AB0C734
00484 433277F09C5C3313E2D1709E7B9E5A7C62ED745C8CE320AE1B59AA930CFF4EEF27FBB6B607F954ECC52C1BE143B687BBFCD24EFB337D1F0B85E4EB1F0BFDA3DB7BDCECF17654E747CB327D1D1B71F35E3F3275F05AFF69C9A990475E97D83D4066D4A056A530384308198476F7821B94D80281317982DBAA3045822B2EC4EC1940FEA030D582BBD205D838401689ACDAE0C72B91CBFCDF6842726541FB3D40AEB32C8B5E4784769C631D8F6F0B85D6D4C331E5703E6AFD34531CA3F45FAED43C6FE56FF4EED16E0A
00485 564C743CFA26C44B7234791F7C4D4BD01F1D6FE16FCF67E6B2BBF3BAA5A7F36A4DC6592824ED10F7900D33548E6304C4708C43DA3CC54953A25B4ED7930C8FB6317B309A73F71791C6989F1B27EAF1ECEEFE9F77AB7E52476EE012C2528CB488445BA26124777817A1ED9E50A22025C05EF565FA0C366C515623E758E133D828B642D7FC941F22702D84F9DC1F4FCED3FDE261BDA72E10D44421BE768635BE4DF11E6577433B458BD37674F27C7B08289CED9F71E68E75CDCE1B4BB1ACF97B0137F372C41AFB96EE
00486 1325895ACDBCCF7C8E4AAF9B9D23120F9F5932A3CF2479635F3E431F2F61B6D0F3C0E583CD5542FEDF3D645DE7F320CD820016G0544797699AFEFB057FF9B8D67EA3711B957FF9B59F327EF23DB397E5BE8CE6E74EDF4D76E54ED741AC79B5508B67A25CF9B2D01F609G0A81CA0B77EDA3AE6F1BA5EAF9C7043CBB6A3D6569C1C6ADD0AB5020DFF9BD875572EA053CBBFD461D9DE44C858A848A76ABAF39D4AD6F2810D71F6FADEF854888850A840A75AB6FF18FF9475C757551AFAB211094831DGEACF70E7E3
00487 776E246B2AC971FEBFFB3FC550EFC80D99224FDB2CA6A5A060E7848B59BCFA9EB22E0DC7AC174D2387G3345A1F6AF430EGF6C4E0F9EC9EAD87EC93C16CBE06158156140058EEB60FD683F617401EE258954AAB4AEDE573E88B4DA74AF81AE11DD41E404E313970C340628476F3061D824CA84AE82FC6F98FA4E05B6F2E227300C99AB13AAC9026581CD227DD39468AF8E0827D0E4651AA741DD7611D3761A3B769D9410843B881C32147AE8D93FBA24DFB3D8A57EC6110B71A7283DE855485444B0C26D5A793B6
00488 1351A24AC82E413D7165A25F1FEAE8BE59AC337D2AD509741B9DBF23AEDFC98F515373BCE5279C862F4C62A96A74397D1C29D55BCFDAD2A151A7F11B2905E7EB122F7D70757949CBF4DE9804F4EAB73B845E4570C0954E576DDFE2739AFD8F0534453AC2A576584D62D3CBF2A119130C58FFB3ACG5E0384769306AD0577D5827B2699631B70E41C173A62557529C871543FA145DFFDB631F92EB72550EB9F62BD061BD4B82F4F9D27F19FC2063430945469CE36562E5F82E3EF8BE20E8654732A409EE82458DCF8
00489 DFAC3038FEEC0BE582EB694736D8A530077B31ADC285F6208D4B089498DF83D3F9A7D2918B98C0F96D82FBFBG65758B6C72G4A3388ECD1BD4A8B91583AFA1437C6E00D27D0DE38402E38D0DE34409E94FD5F309531F7C45F778A6C63FA14F7D5E04BE414A78B2CA79F652D94583D79A8AFCCE0B179A8AFC2E0B689654588EC11502FB5CD54D768B7A830C6215F1840AE087A5ECE43315A4E7664D4E118611259EA325D04E1C9EF534BCEC3F3DBCFD7E7CF4B154E0EABCD6D70016FFB3FC4547B5EA4A4486F3E77
00490 6AB4EE5F6B14E7CC767AA49E5B5D4B7C936549CB87BF13CE7D497EEA753EBC557151843E2E646997BD52697C3E1F28536F74C8273A36A42A537F45A31D6ADC267073FA15FF0CE72B3D473ECDCA3F7C095F6FCC8526737A04A84F200C75C901F3AB93F83B6E2D21EB93596112385C4A936A76DA36673AAE4E0F5C4D0ABC1221BCC9050E775FG0B4DEB81EF4D40BE8DBB4A6C815E67886C52F16C7BA0013575E15FAF4FC03F54F8298A1E61703E19664B041884289D4884F49BA8GA898E8A5D0B8D0ECA67276B1DE
00491 FA4F005EC920670585D9056CBE81BD5B277785681D06FA40681D00C1F84E49C25EBB7BD6E8545B1B42B35CFE116AC21FABB3BDFDE50E729E2C680CF80072F9F3062FEF1DAD552A64367B3443E3B32A0BFA0D0777003D6F4C633DFFFA7FC0FDCFF91B4AD67F27F5D15F6327F1G7DFE41AE0273F2AC734D93D6E942E6B58F73793D0979165F82AD4EC21F715D81E65B907073395D350F8899566374AE4410F1F8FC54E1F3D9CD98A7C4723992E404GD5ED23588F4D4D0AAE11D95AB1261AE2A1CF96706DD05A22F8
00492 9B1F7FA8F19B9F0D4771B1398D6D7E7F46235D4F5B06FD7676E92AFF18F8CFE8206F746E8DFF7F7B535EEBFC1A77FF5A766AFE5EC602FC4A78BCF768273237EC72A02B578884D83C8F1631B9FFB35405ECAFD4623E3B9AB06E2B852C95E88CE89E50126D585F4B9A33181CE11733F1F8D83250B8536660B2FF41E206A701D6C1FE0E9DE2314093345DG63B6F2DECFED04277FBBCB0F04344D5B51966A5B509674595A3610293285EA871476A936D01B6D3685DEC6B6ABE3BDD0C3B66AF020502DC351E5E69710B6
00493 180DBADC9FC09D667951E10B068EE80F0BFCF4F8124D419B0016889DAA0B5CBADCE3B149F2C8DBA9F43861C29D227D6810BC058E09B95EBABC45465D0BB4EF8E6A103C5F2D43DC26239E52AAF2D0071F4B28C3FF0E368EC9D368E0715161B60BED1E811A94BA3C2852213000264F0334G2143D7A454E1059F9D322750A154C707A7D9BBBC8F34CE687023E2D5DF30F6080634D8214318680B529D5ABA6C1CC2077A9DEE9D789E3769GAD2395F09390DF63E66EAD07E71F711A6F6DABG3B9CB6D8554937B84AEE
00494 BDAA7E631DD91D25226F073E6F4578A6607B7710FE4BF53FF74766AAF58ED21ED5E4FDD206284BAFCB285F880534E8201CDC309F2086207EDC2CDB5FDE2AA3BD1982759BE559B8BC46EE4D6101953DC0660669E2144BFE63A055D4797E6F5E837E5A87A41C033835F3681AB4AC779AC705DD58EB69B940104D41B60CA2F2D9DCD80BFE4E826FF30116832D866A957728FEFF1472D90C37ECAE9979F447102FE2E7A1E98632G4D594979386DFC0545DB010085812D59C9312BFDF99AED6AE93F23FFE6E701F847C7
00495 601339F4FD6CFB13DEFCCF6198CD470B7A6ACDD31E5E477A1A26379B07A40B10DB54CD57076A1B6D9C7FE98E4555B73BB97EE49D1D4B5DB755D14E9B9729FC71CD83A15F5515466B53EE9B353122B9FE2F054AF15FCA97FB9899B436D12A6831774B53DFBE350D590F38D86E447A70BBBC6FB42AE3793CBC5EA7757064694F16E825F741131FD3BF3EDB6B1C5A846913C2C62BC5CB4602BC1C9BAF1F244F0356030ACFA920BF8920248518697CE415EE6A45A53CA61B4566A82D292A2DE0F474E8995E93B463DECD
00496 D09E1F5728FFCBA16EBFAD0C173919154947F7019347F75407779153EF676B767B995F61F9FCDCD76CF22FB3825BA36382F7D17BDD904FE222DD688BFF960F3EB0FC172FAF44FD881C2723A1CF62EE6E8B59774BF73BFDA1EF1B3201AC158D638582DE1FED556EB6149ACA3C5B70AC84B425C590235A1CF66330E4AA2A50D7D5682BEB4A704C607B8D5816453BF1DD392141FBDD799AD12F8BF7B5FA2FAB63BC52BFEA74DED71E0CD327FF5A683D2EC4FEDE0F08C6E6A7C387157746FE76EEC43BB9D7632E736E36
00497 195B4DC49B56F5F0B74EEBC5C75C328E71F29CD8CEFE2DBB2DF3E06665FCEBG4B899065ECD2498A2FE765B8311C28236E34DE574C4B79368B4BD9AD4AD9F94CAD6B85BE5EECD84E3F9EF727FDC71EF9B931B21613180F65ACBC6116750F792C1CB1AC67EBFFF2271924191773A3894B2997650C54295A0D57E7824B39F2521DF6F6966DF61FE8B7D914F31C3A82BC0BB9C06DD21C0570D0824FE28ED05B255F3FB49BAD66CF58A6B23F5A4B676364D3B4BD184A850A82A285609F8BF01E5FFC00863574D79AFC67
00498 7896532804FBC9D85E2FCB7C1FA53DD0B27D6FB9ECA8E1EBCC9B4CA593D4BE629BCBE8ECA45B6C8CD44E6958190C43BCBAA6732C8A9ED34276CD249186737D536F57627EE99554ED2CG774C1374B48671BE2FB470G232E2EC59E9E13CCE714F0C3690FBF56625E566282BC37BCF0144A8F0377E82014BD050A4F7EA481FDF6EC59BF910B6E6B1AFBCE850F4F556977F05F5B3C476D33EFBF5C194C75B79C435F691983694B77207E55D78B547AD3C32A2B7B50E1B61DB10E3633E8076BFC63986A9C3D87F58EE2
00499 B2CB77C2EC87543F97ED6B318F5CF67AC15FCC6C1457751747547393555F5F7E1AFDAF2FE340DEF7DD5137A610CDA3FE4E32D908406BD3FD864F32C3C18647528FA216368F31CD3B71AEDA73BE2C7732B1DA6F5B709EG94AC72FEE6413CAB77617EC114D99D0B47821E251FFA3F000F2BCD27691CDA8CF99B00CCC0370196GAD818A81DA839481948B14D3D8C8CA016A013A002E8249C0738AF19C7E291C6EE57ADBCBA89D4E862343486F52707EFBB83E941E5C004FC224E5F35CB230DFBD115AEDB769776D4E
00500 40D835707452B25E0F730E2877B3A35ABE55A5786947C5054A9EDD21777E6F3B62ECBF3CD0AB6609BE2D05F17B7B280B90F11F4D635CBF27885A29E86A7667FC0EB6B5DFBD70F44D086F5B83EABE9370CC4E08AF5825661B8FBC0BE744976741378CF8D64D08AFC4D2730583CF740C789E74A8AFF1FFA1495BBFB51F3216BD655F2F671E1A5E2F6FE37BA19278635EDBF6658C3F78943B67B5B26214447CD1F6AACBE0ED4EAE1B53CCE7AC2E7B2335532D0BAB3C6A42791E1816EF2FE6DB45CE4B67CD7C8C6FBEB6
00501 97346EF747459C7F9643FBD5B8776D65C75137DF053415C05C0798AED0BFD8DA8CEBD320C1A099A8GE8E9B17A059F1F22FB75D35E9D6D35595B69A0D7DDEB63752BBD7679FEBF6B4C67647B4B2C79143B5947E97B2CAC76EE4FC2062FA976EE4FFF96F3E5B824B59C40761C57CD5BB3885ED7GC5G4582E51500CFA941760CBBCD83ECFFFE365BE6E3275974E09B5C2C64D0F9DC45E61ABD7CCE893747AE65E90267E409160DEEE7F7BE67ABE90B1567B265392A44F70CF23E185DD8DEB86409764A17F8505F79
00502 F3291936D15EC16F73679A06179E74BEFFFEEC8C632793103668A04E0FF3ADDAFD8A1399FB66403334546BDC075F9F3C464E2DCB8BD5FB7CA98C6BD5B05E9F498D7E7D4EBD9D537B1D7BBB34634907BAFC634907BB346349608EF5BC4931C7BA685CB68A73EE3F4877C3018D886CF1A613E2174CA6F9CC60BFE5FAD13CD52285A27E94536BA6437A95EC358A9BD030E7BA286F04AA0F5944FD58E7BB58190059E2616F3FE1F94CD6F02522BDDEE4BA1A6DC6155E918223FA7331725D9EAA4BDE0A634259D9B44538
00503 E0FBD5ECD501F6C99254F6B197648416CEBD4FF09B78F9835A85DD03F3ECCD835A45EBA25FDDED3E767335B6357DF06C47833E791E98704D77044BB75FAA17EF3EBC0DFCFBB4722D15FC7305C93E799E5510771807BCFEB7F4C5F6BA6BCB0B19FA9F764BF64287FC132D477967A52A4F55C77F5677D9FD7D4F39AF348CEEFB47AF7877819FDC503E1F58FCC17B1E77398BD37F7ED177857F3FFFB4F0C17D7BC74ABD65636E76BE287A3C7458975F76CFFF21E570BA5F5D6D3F6D833B27773F8FF5EB7B5FEFF77B7A
00504 5F60EEED7F7B03EE357F65E3A43B05E241B0C6D6170ABBBFADF8D7E61D40D6346099F114409CECFF283E2C107416A1D646560EE370BEA930D29D1EB94F97182C43B29689EC238E4BD8A230CCF6AE96836F8507909BE3D8953C778B6C5F72453D27C3B8279A4C5477060877936CBDCC3C2F98D377BB4D7737372D67BC4A78DB1EDFD362F53F5F02ED99AB5AA356026D11D20ED8E29176D7FFB96EFB9859F72315FDADB635F23CE0B25D0D63542A585177FB68FC68D466A9AEFBE7022F7FADC8D07BDFE52F35057A8D
00505 1359E93798EFC926734AC58A02E70C4DADF8D6EEA947FD147F57CBE8FF33BD76DF37609E7B6DF26DBDF6CAF8763AG7284153B77581717FB6F315FA5335F2530B9A44F3B988FB15BDE8979571463B9C643C1EABF66E11B156769E3369E8D6931C07CCC60020E1D89D4206E8FDEF46B1E180C3A87D6E81F15EEA55A6777D45F608AEF5DCB7269596A8D49A11B070D96FEB8F446686832D94C433714FAB432F1F118563D826B71D9BE0DCDA060B1FFC263EF9FCEEC037B996FE9BA7EAA700C6339FC2C4309435A6D0F
00506 E74E548735C31E2B075D6DAF9F762E4360956A975D87DB7C37E9785913592CBEFB1A833C740ED490BC179F46763D5167EE5F6C8954ED0D9F5D3629ECA38272449CF61FC527993C4F438F97218D6499306DBEEE41B38A3EBF13F29677E7CE98E63ABF03E7D29D175C1FBF26EEC2A923127DAE0167BE21E148E29C9E67F9DF9AF0674D508D92773EA2EE3B36CD98C725B6B054D2FA751FCE5C25E5867858AD71EF931496D5CAA6D7653853D5B9ECF6D6AA3FC6DEB964B2D71AA92B33322B2F47B0EA9EA9AAABD34EE1
00507 F57440D9EB7F2B5BE8F6FAEDFFA9EDF3B4995B46EE407E7A174BEE5D7B732B09673DCA5537DB8CFDAD5D3DEDCD0D6DD7FA1A3ABB5B5B4FB4F6DFE9EC3F54B850A378FF10DFB385FFEBE7F75B654E0EDE8F899DADA096771FD38BD03FA5B36EBB5CDB3B7BE3A2EC695ADF7C6C33B2E366E5BDE446BD51F5865CBFDDB84E560E15B03600DAABF17F34F982753ADAB9DB1BFAFD505D3EFDC57E6C084FCD69E755EB0BC0A8AB38F2A6FBDFF549EA3E954093BAA33E0505EA3EC860091D915F43EC6FB82BCABBEF3197FE
00508 825E799AFC0B0536EFFB1577FE47F60677D7F96FF75CBF0E7B9DA6C8DBD505F1C25B04475D746AC252D0BD13B5D871D95FB9316C2C6F5A65C232EF3E3EE45FFC41053E799EA9744D772F4C56FAC1C7FBB54E7DB957B09E18AB30236394DB826FEB2A312E19746A0072B9CF75792171AFBE8EFF6C8BAD0357796A04EF9BCA933EF1CA28197298DD328DFC267993096E84623C30D15CC3082846BB026557F02EAA2EA9A4A7007A01A60182EB44BD72715D0A4CA666B9E1C03AA62C4E338E5B845BE8C479E32CDFD83C
00509 A2F8932F7978CA66DD8C0D97FBBB2FF4377434DDEE3952F371CCCF4B050BAD9D3DD71ABA5BAF1E6F203E127B148B57705CEAD58D1E77FFF64D7B3C7FEE0F737AC72ECDFD5E7F72B56F73FECF7E9D63D31F77FFB60E773F157B5257E63B2F497FCF1587BAB7C0C09A3C11A449A4DFF595C62FDC1B51AB3FAAA713048E69A67C5BE8B249A4395BE55543B4A713D4FA5DC7EFF49A8C8619A4523BBC7020D7F1E42263B7FE1C8E126169C7637E4F4EAFE77D4391D7BC511DA53A912345BEE6ECA3C96C47E55AC97C3093
00510 D4E13F82D589AC1543142512B176507B98A7BFA6DBC69C23C3AC3BCC62BFBE7BB188E1EF5749DFC9EABBC91547586EA82C8AE53253AD290B6E11AA89A7A769EFA91377D72FFE5F8EFF20E426D0320D6DD62D3BF124AE6165FFCA08A709EDC447D70FEDA411AE81C1D936C2ECA38930FA641260AFD521A410166EF11D6449070E3E327A05BEE782513511DD7446EC0F64E007611209FE79D679857F33E40B1DFE690C7EC0B19465E40FA427FC4B826D12B352CDFF2150A9CB26C65CBA00165A416B67124D164AD623
00511 F3CC2616FD321DA4DA697FB5C03673E47AF3DA154A4FE9B1FD639A9B184E54EB9350B71B69CB259804146C47B38F941E0BD81EC0624F12D40B4DE86251CB9B59A20FB9A467184DE21A341F6602D2EE52C14202F09017AF2ACFABEBE077EFD0697149876627C7261F0DA7E452C1AAD9CE5AA586114354B4E624F6A8B95AE4FE9938D824FDE92FDC720B8FF78E4613B82512345737CD5AE5EACA93E64BADB04A7362720E13266E10C1E307516A243FD9865A693D3443A4D108619F1F2EDA781DF7AE33C25C2CB25967
00512 3626D149B6D159B8B2E206409BB3C05B0278BDC2BC4DE3704A33FD726E9D677E637DA13005E612B0D1D5457E2DE67F5650FF2B99D24D106A9AE860E8B2651FF77AA45619991030EC760BEAE72197655FECFC7ADB4F57C7C7C16D4EAA438EBAA24B1D2B43B5B1A4B93E923CF04F5600F5FFCF7B49CE4DE5124A5D454527F80C9E0A24FB0D02549966CB7ADF18AFF51672689FB850D4FA5FCCCF37C66BE47AE575F4755D423AE9DB89C871C57B0741EE4CC39386570D8903F1C8B6C8A633EC205FBCB609654965A72E
00513 AE9FFBFAC7D1BCC9EAA3DBC74C1245544396A86DA40B3DB5CB4EE10759CE8BE7C3241DECE3B8AEE4BAF06C3413EC957BD933C5323A13B2D4C9973B5BE512410700D512AB61DD71A6B229B698864F703550A02C0F86E1FDB4886B23C1E5FDB4886B23C13EBE9AD456C7B2B9B8431594D5255E335571AF53274F0868B31F36D66E080434286F9694645C61773BE50B6B14B330BA779D91FEB6718FBDEC7F82703413F8BE71E2B75DAB70F71738E742E83148C64BF82355C46F951F39A5CB6EBD5F009EAA5F09F914C4
00514 657C28076AFDCD45737F81D0CB87884D019C7B19A4GGECEDGGD0CB818294G94G88G88G0ED1CCA94D019C7B19A4GGECEDGG8CGGGGGGGGGGGGGGGGGE2F5E9ECE4E5F2A0E4E1F4E1D0CB8586GGGG81G81GBAGGG53A4GGGG
00515 **end of data**/
00516 }
00517 /**
00518 * Return the JDialogContentPane property value.
00519 * @return javax.swing.JPanel
00520 */
00521 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00522 private javax.swing.JPanel getJDialogContentPane() {
00523 if (ivjJDialogContentPane == null) {
00524 try {
00525 ivjJDialogContentPane = new javax.swing.JPanel();
00526 ivjJDialogContentPane.setName("JDialogContentPane");
00527 ivjJDialogContentPane.setBorder(new javax.swing.border.EtchedBorder());
00528 ivjJDialogContentPane.setLayout(new java.awt.GridBagLayout());
00529 ivjJDialogContentPane.setBackground(new java.awt.Color(204,204,255));
00530
00531 java.awt.GridBagConstraints constraintsPVSButton = new java.awt.GridBagConstraints();
00532 constraintsPVSButton.gridx = 1; constraintsPVSButton.gridy = 4;
00533 constraintsPVSButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00534 constraintsPVSButton.insets = new java.awt.Insets(5, 10, 0, 10);
00535 getJDialogContentPane().add(getPVSButton(), constraintsPVSButton);
00536
00537 java.awt.GridBagConstraints constraintsAddToLibraryButton = new java.awt.GridBagConstraints();
00538 constraintsAddToLibraryButton.gridx = 1; constraintsAddToLibraryButton.gridy = 7;
00539 constraintsAddToLibraryButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00540 constraintsAddToLibraryButton.anchor = java.awt.GridBagConstraints.SOUTH;
00541 constraintsAddToLibraryButton.insets = new java.awt.Insets(10, 10, 0, 10);
00542 getJDialogContentPane().add(getAddToLibraryButton(), constraintsAddToLibraryButton);
00543
00544 java.awt.GridBagConstraints constraintsBASLCodeScrollPane = new java.awt.GridBagConstraints();
00545 constraintsBASLCodeScrollPane.gridx = 0; constraintsBASLCodeScrollPane.gridy = 1;
00546 constraintsBASLCodeScrollPane.gridheight = 7;
00547 constraintsBASLCodeScrollPane.fill = java.awt.GridBagConstraints.BOTH;
00548 constraintsBASLCodeScrollPane.weightx = 1.0;
00549 constraintsBASLCodeScrollPane.weighty = 1.0;
00550 constraintsBASLCodeScrollPane.insets = new java.awt.Insets(5, 10, 0, 0);
00551 getJDialogContentPane().add(getBASLCodeScrollPane(), constraintsBASLCodeScrollPane);
00552
00553 java.awt.GridBagConstraints constraintsBASLLabel = new java.awt.GridBagConstraints();
00554 constraintsBASLLabel.gridx = 0; constraintsBASLLabel.gridy = 0;
00555 constraintsBASLLabel.gridwidth = 2;
00556 constraintsBASLLabel.fill = java.awt.GridBagConstraints.BOTH;
00557 constraintsBASLLabel.weightx = 1.0;
00558 constraintsBASLLabel.insets = new java.awt.Insets(10, 10, 0, 10);
00559 getJDialogContentPane().add(getBASLLabel(), constraintsBASLLabel);
00560
00561 java.awt.GridBagConstraints constraintsSaveAsButton = new java.awt.GridBagConstraints();
00562 constraintsSaveAsButton.gridx = 1; constraintsSaveAsButton.gridy = 3;
00563 constraintsSaveAsButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00564 constraintsSaveAsButton.insets = new java.awt.Insets(5, 10, 0, 10);
00565 getJDialogContentPane().add(getSaveAsButton(), constraintsSaveAsButton);
00566
00567 java.awt.GridBagConstraints constraintsRemoveButton = new java.awt.GridBagConstraints();
00568 constraintsRemoveButton.gridx = 1; constraintsRemoveButton.gridy = 11;
00569 constraintsRemoveButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00570 constraintsRemoveButton.insets = new java.awt.Insets(5, 10, 10, 10);
00571 getJDialogContentPane().add(getRemoveButton(), constraintsRemoveButton);
00572
00573 java.awt.GridBagConstraints constraintsOpenButton = new java.awt.GridBagConstraints();
00574 constraintsOpenButton.gridx = 1; constraintsOpenButton.gridy = 2;
00575 constraintsOpenButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00576 constraintsOpenButton.insets = new java.awt.Insets(5, 10, 0, 10);
00577 getJDialogContentPane().add(getOpenButton(), constraintsOpenButton);
00578
00579 java.awt.GridBagConstraints constraintsNewButton = new java.awt.GridBagConstraints();
00580 constraintsNewButton.gridx = 1; constraintsNewButton.gridy = 1;
00581 constraintsNewButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00582 constraintsNewButton.insets = new java.awt.Insets(5, 10, 0, 10);
00583 getJDialogContentPane().add(getNewButton(), constraintsNewButton);
00584
00585 java.awt.GridBagConstraints constraintsPVSLogoLabel = new java.awt.GridBagConstraints();
00586 constraintsPVSLogoLabel.gridx = 1; constraintsPVSLogoLabel.gridy = 5;
00587 constraintsPVSLogoLabel.anchor = java.awt.GridBagConstraints.SOUTH;
00588 constraintsPVSLogoLabel.insets = new java.awt.Insets(15, 0, 0, 0);
00589 getJDialogContentPane().add(getPVSLogoLabel(), constraintsPVSLogoLabel);
00590
00591 java.awt.GridBagConstraints constraintsShowButton = new java.awt.GridBagConstraints();
00592 constraintsShowButton.gridx = 1; constraintsShowButton.gridy = 9;
00593 constraintsShowButton.fill = java.awt.GridBagConstraints.HORIZONTAL;
00594 constraintsShowButton.insets = new java.awt.Insets(5, 10, 0, 10);
00595 getJDialogContentPane().add(getShowButton(), constraintsShowButton);
00596
00597 java.awt.GridBagConstraints constraintsLibraryScrollPane = new java.awt.GridBagConstraints();
00598 constraintsLibraryScrollPane.gridx = 0; constraintsLibraryScrollPane.gridy = 9;
00599 constraintsLibraryScrollPane.gridheight = 4;
00600 constraintsLibraryScrollPane.fill = java.awt.GridBagConstraints.BOTH;
00601 constraintsLibraryScrollPane.weightx = 1.0;
00602 constraintsLibraryScrollPane.weighty = 1.0;
00603 constraintsLibraryScrollPane.insets = new java.awt.Insets(5, 10, 10, 0);
00604 getJDialogContentPane().add(getLibraryScrollPane(), constraintsLibraryScrollPane);
00605
00606 java.awt.GridBagConstraints constraintsAbstractionsLabel = new java.awt.GridBagConstraints();
00607 constraintsAbstractionsLabel.gridx = 0; constraintsAbstractionsLabel.gridy = 8;
00608 constraintsAbstractionsLabel.gridwidth = 2;
00609 constraintsAbstractionsLabel.fill = java.awt.GridBagConstraints.HORIZONTAL;
00610 constraintsAbstractionsLabel.weightx = 1.0;
00611 constraintsAbstractionsLabel.insets = new java.awt.Insets(10, 10, 0, 10);
00612 getJDialogContentPane().add(getAbstractionsLabel(), constraintsAbstractionsLabel);
00613 // user code begin {1}
00614 // user code end
00615 } catch (java.lang.Throwable ivjExc) {
00616 // user code begin {2}
00617 // user code end
00618 handleException(ivjExc);
00619 }
00620 }
00621 return ivjJDialogContentPane;
00622 }
00623 /**
00624 * Return the LibraryScrollPane property value.
00625 * @return javax.swing.JScrollPane
00626 */
00627 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00628 private javax.swing.JScrollPane getLibraryScrollPane() {
00629 if (ivjLibraryScrollPane == null) {
00630 try {
00631 ivjLibraryScrollPane = new javax.swing.JScrollPane();
00632 ivjLibraryScrollPane.setName("LibraryScrollPane");
00633 ivjLibraryScrollPane.setVerticalScrollBarPolicy(javax.swing.JScrollPane.VERTICAL_SCROLLBAR_ALWAYS);
00634 ivjLibraryScrollPane.setHorizontalScrollBarPolicy(javax.swing.JScrollPane.HORIZONTAL_SCROLLBAR_NEVER);
00635 getLibraryScrollPane().setViewportView(getScrollPaneTable());
00636 // user code begin {1}
00637 // user code end
00638 } catch (java.lang.Throwable ivjExc) {
00639 // user code begin {2}
00640 // user code end
00641 handleException(ivjExc);
00642 }
00643 }
00644 return ivjLibraryScrollPane;
00645 }
00646 /**
00647 * Return the NewButton property value.
00648 * @return javax.swing.JButton
00649 */
00650 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00651 private javax.swing.JButton getNewButton() {
00652 if (ivjNewButton == null) {
00653 try {
00654 ivjNewButton = new javax.swing.JButton();
00655 ivjNewButton.setName("NewButton");
00656 ivjNewButton.setMnemonic('n');
00657 ivjNewButton.setText("New");
00658 ivjNewButton.setBackground(new java.awt.Color(204,204,255));
00659 // user code begin {1}
00660 // user code end
00661 } catch (java.lang.Throwable ivjExc) {
00662 // user code begin {2}
00663 // user code end
00664 handleException(ivjExc);
00665 }
00666 }
00667 return ivjNewButton;
00668 }
00669 /**
00670 * Return the OpenButton property value.
00671 * @return javax.swing.JButton
00672 */
00673 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00674 private javax.swing.JButton getOpenButton() {
00675 if (ivjOpenButton == null) {
00676 try {
00677 ivjOpenButton = new javax.swing.JButton();
00678 ivjOpenButton.setName("OpenButton");
00679 ivjOpenButton.setMnemonic('o');
00680 ivjOpenButton.setText("Open");
00681 ivjOpenButton.setBackground(new java.awt.Color(204,204,255));
00682 // user code begin {1}
00683 // user code end
00684 } catch (java.lang.Throwable ivjExc) {
00685 // user code begin {2}
00686 // user code end
00687 handleException(ivjExc);
00688 }
00689 }
00690 return ivjOpenButton;
00691 }
00692 /**
00693 * Return the JButton1 property value.
00694 * @return javax.swing.JButton
00695 */
00696 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00697 private javax.swing.JButton getPVSButton() {
00698 if (ivjPVSButton == null) {
00699 try {
00700 ivjPVSButton = new javax.swing.JButton();
00701 ivjPVSButton.setName("PVSButton");
00702 ivjPVSButton.setMnemonic('r');
00703 ivjPVSButton.setText("Run PVS");
00704 ivjPVSButton.setBackground(new java.awt.Color(204,204,255));
00705 // user code begin {1}
00706 if (System.getProperty("os.name").indexOf("Windows") >= 0) {
00707 ivjPVSButton.setEnabled(false);
00708 ivjPVSButton.setToolTipText("PVS is not available for Windows-based system");
00709 }
00710 // user code end
00711 } catch (java.lang.Throwable ivjExc) {
00712 // user code begin {2}
00713 // user code end
00714 handleException(ivjExc);
00715 }
00716 }
00717 return ivjPVSButton;
00718 }
00719 /**
00720 * Return the PVSLogoLabel property value.
00721 * @return javax.swing.JLabel
00722 */
00723 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00724 private javax.swing.JLabel getPVSLogoLabel() {
00725 if (ivjPVSLogoLabel == null) {
00726 try {
00727 ivjPVSLogoLabel = new javax.swing.JLabel();
00728 ivjPVSLogoLabel.setName("PVSLogoLabel");
00729 ivjPVSLogoLabel.setIcon(new javax.swing.ImageIcon(getClass().getResource("/edu/ksu/cis/bandera/bui/images/PVS.gif")));
00730 ivjPVSLogoLabel.setBorder(BorderFactory.createRaisedBevelBorder());
00731 ivjPVSLogoLabel.setText("");
00732 // user code begin {1}
00733 // user code end
00734 } catch (java.lang.Throwable ivjExc) {
00735 // user code begin {2}
00736 // user code end
00737 handleException(ivjExc);
00738 }
00739 }
00740 return ivjPVSLogoLabel;
00741 }
00742 /**
00743 * Return the RemoveButton property value.
00744 * @return javax.swing.JButton
00745 */
00746 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00747 private javax.swing.JButton getRemoveButton() {
00748 if (ivjRemoveButton == null) {
00749 try {
00750 ivjRemoveButton = new javax.swing.JButton();
00751 ivjRemoveButton.setName("RemoveButton");
00752 ivjRemoveButton.setMnemonic('m');
00753 ivjRemoveButton.setText("Remove");
00754 ivjRemoveButton.setBackground(new java.awt.Color(204,204,255));
00755 // user code begin {1}
00756 // user code end
00757 } catch (java.lang.Throwable ivjExc) {
00758 // user code begin {2}
00759 // user code end
00760 handleException(ivjExc);
00761 }
00762 }
00763 return ivjRemoveButton;
00764 }
00765 /**
00766 * Return the SaveAsButton property value.
00767 * @return javax.swing.JButton
00768 */
00769 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00770 private javax.swing.JButton getSaveAsButton() {
00771 if (ivjSaveAsButton == null) {
00772 try {
00773 ivjSaveAsButton = new javax.swing.JButton();
00774 ivjSaveAsButton.setName("SaveAsButton");
00775 ivjSaveAsButton.setMnemonic('s');
00776 ivjSaveAsButton.setText("Save as...");
00777 ivjSaveAsButton.setBackground(new java.awt.Color(204,204,255));
00778 // user code begin {1}
00779 // user code end
00780 } catch (java.lang.Throwable ivjExc) {
00781 // user code begin {2}
00782 // user code end
00783 handleException(ivjExc);
00784 }
00785 }
00786 return ivjSaveAsButton;
00787 }
00788 /**
00789 * Return the ScrollPaneTable property value.
00790 * @return javax.swing.JTable
00791 */
00792 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00793 private javax.swing.JTable getScrollPaneTable() {
00794 if (ivjScrollPaneTable == null) {
00795 try {
00796 ivjScrollPaneTable = new javax.swing.JTable();
00797 ivjScrollPaneTable.setName("ScrollPaneTable");
00798 getLibraryScrollPane().setColumnHeaderView(ivjScrollPaneTable.getTableHeader());
00799 getLibraryScrollPane().getViewport().setBackingStoreEnabled(true);
00800 ivjScrollPaneTable.setAutoResizeMode(javax.swing.JTable.AUTO_RESIZE_SUBSEQUENT_COLUMNS);
00801 ivjScrollPaneTable.setBounds(0, 0, 200, 200);
00802 ivjScrollPaneTable.setAutoCreateColumnsFromModel(true);
00803 // user code begin {1}
00804 // user code end
00805 } catch (java.lang.Throwable ivjExc) {
00806 // user code begin {2}
00807 // user code end
00808 handleException(ivjExc);
00809 }
00810 }
00811 return ivjScrollPaneTable;
00812 }
00813 /**
00814 * Return the ShowButton property value.
00815 * @return javax.swing.JButton
00816 */
00817 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00818 private javax.swing.JButton getShowButton() {
00819 if (ivjShowButton == null) {
00820 try {
00821 ivjShowButton = new javax.swing.JButton();
00822 ivjShowButton.setName("ShowButton");
00823 ivjShowButton.setMnemonic('h');
00824 ivjShowButton.setText("Show");
00825 ivjShowButton.setBackground(new java.awt.Color(204,204,255));
00826 // user code begin {1}
00827 // user code end
00828 } catch (java.lang.Throwable ivjExc) {
00829 // user code begin {2}
00830 // user code end
00831 handleException(ivjExc);
00832 }
00833 }
00834 return ivjShowButton;
00835 }
00836 /**
00837 * Called whenever the part throws an exception.
00838 * @param exception java.lang.Throwable
00839 */
00840 private void handleException(java.lang.Throwable exception) {
00841
00842 /* Uncomment the following lines to print uncaught exceptions to stdout */
00843 // System.out.println("--------- UNCAUGHT EXCEPTION ---------");
00844 // exception.printStackTrace(System.out);
00845 }
00846 /**
00847 *
00848 */
00849 private static void init() {
00850 try {
00851 abstractionPackage = Preferences.getAbstractionPackage();
00852 abstractionPath = Preferences.getAbstractionPath();
00853 abstractionListPath = abstractionPath + File.separator + "Abstractions";
00854 LineNumberReader r = new LineNumberReader(new FileReader(abstractionListPath));
00855 String abstraction;
00856 while ((abstraction = r.readLine()) != null) {
00857 abstraction = abstraction.trim();
00858 if (!"".equals(abstraction))
00859 abstractions.add(abstraction);
00860 }
00861 r.close();
00862 } catch (Throwable e) {
00863 System.out.println("Cannot load abstractions...");
00864 e.printStackTrace();
00865 }
00866 }
00867 /**
00868 * Initializes connections
00869 * @exception java.lang.Exception The exception description.
00870 */
00871 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00872 private void initConnections() throws java.lang.Exception {
00873 // user code begin {1}
00874 // user code end
00875 getNewButton().addActionListener(ivjEventHandler);
00876 getAddToLibraryButton().addActionListener(ivjEventHandler);
00877 getPVSButton().addActionListener(ivjEventHandler);
00878 getSaveAsButton().addActionListener(ivjEventHandler);
00879 getOpenButton().addActionListener(ivjEventHandler);
00880 getShowButton().addActionListener(ivjEventHandler);
00881 getRemoveButton().addActionListener(ivjEventHandler);
00882 }
00883 /**
00884 * Initialize the class.
00885 */
00886 /* WARNING: THIS METHOD WILL BE REGENERATED. */
00887 private void initialize() {
00888 try {
00889 // user code begin {1}
00890 // user code end
00891 setName("AbtractionLibraryManager");
00892 setDefaultCloseOperation(javax.swing.WindowConstants.DISPOSE_ON_CLOSE);
00893 setSize(546, 474);
00894 setModal(true);
00895 setTitle("Abstraction Library Manager");
00896 setContentPane(getJDialogContentPane());
00897 initConnections();
00898 } catch (java.lang.Throwable ivjExc) {
00899 handleException(ivjExc);
00900 }
00901 // user code begin {2}
00902 updateAbstractionTable();
00903 // user code end
00904 }
00905 /**
00906 * main entrypoint - starts the part when it is run as an application
00907 * @param args java.lang.String[]
00908 */
00909 public static void main(java.lang.String[] args) {
00910 try {
00911 AbstractionLibraryManager aAbstractionLibraryManager;
00912 aAbstractionLibraryManager = new AbstractionLibraryManager();
00913 aAbstractionLibraryManager.setModal(true);
00914 aAbstractionLibraryManager.addWindowListener(new java.awt.event.WindowAdapter() {
00915 public void windowClosing(java.awt.event.WindowEvent e) {
00916 System.exit(0);
00917 };
00918 });
00919 aAbstractionLibraryManager.setVisible(true);
00920 } catch (Throwable exception) {
00921 System.err.println("Exception occurred in main() of javax.swing.JDialog");
00922 exception.printStackTrace(System.out);
00923 }
00924 }
00925 /**
00926 * Comment
00927 */
00928 public void newButton_ActionEvents() {
00929 return;
00930 }
00931 /**
00932 * Comment
00933 */
00934 public void openButton_ActionEvents() {
00935 FileChooser.chooser.setCurrentDirectory(new File(System.getProperty("user.dir")));
00936 FileChooser.chooser.setFileFilter(FileChooser.BASL);
00937 FileChooser.chooser.setSelectedFile(new File(""));
00938 FileChooser.chooser.setFileSelectionMode(FileChooser.FILES_ONLY);
00939 if (FileChooser.chooser.showOpenDialog(this) == FileChooser.APPROVE_OPTION) {
00940 File file = FileChooser.chooser.getSelectedFile();
00941 if (!file.exists()) {
00942 JOptionPane.showMessageDialog(this, "File is not exist", "Open Error", JOptionPane.ERROR_MESSAGE);
00943 return;
00944 }
00945 try {
00946 FileReader r = new FileReader(file);
00947 AbstractionGenerator ag = new AbstractionGenerator(new PushbackReader(r));
00948 getBASLCodeTextArea().setText(AbstractionPrinter.print(ag.getNode(), true));
00949 r.close();
00950 } catch (Exception e) {
00951 JOptionPane.showMessageDialog(this, e.getMessage(), "Open Error", JOptionPane.ERROR_MESSAGE);
00952 }
00953 }
00954 }
00955 /**
00956 * Comment
00957 */
00958 public void pVSButton_ActionEvents() {
00959 try {
00960 AbstractionGenerator ag = new AbstractionGenerator(new StringReader(getBASLCodeTextArea().getText()));
00961 String s = ag.generate(abstractionPackage);
00962 ag.getErrors().remove("Default token is undefined");
00963 if (ag.getErrors().size() > 0) {
00964 StringBuffer buffer = new StringBuffer("Errors:\n");
00965 for (Iterator i = ag.getErrors().iterator(); i.hasNext();) {
00966 buffer.append("- " + i.next() + "\n");
00967 }
00968 if (ag.getWarnings().size() > 0) {
00969 buffer.append("Warnings:\n");
00970 for (Iterator i = ag.getWarnings().iterator(); i.hasNext();) {
00971 buffer.append("- " + i.next() + "\n");
00972 }
00973 }
00974 JOptionPane.showMessageDialog(this, buffer.toString(), "Cannnot run PVS", JOptionPane.ERROR_MESSAGE);
00975 return;
00976 }
00977 Reader r = new StringReader(AbstractionPrinter.print(ag.getNode(), false));
00978 parser parserObj = new parser(new Yylex(r));
00979 parserObj.parse();
00980 r.close();
00981 if (parserObj.npredicates != parserObj.tokens.size()) {
00982 JOptionPane.showMessageDialog(this, "Wrong token set", "Cannnot run PVS", JOptionPane.ERROR_MESSAGE);
00983 return;
00984 }
00985 new File("abstraction.pvs").delete();
00986 new File("abstraction.prf").delete();
00987 new File("abstraction.el").delete();
00988 PrintWriter pwPVS = new PrintWriter(new FileWriter("abstraction.pvs"));
00989 PrintWriter pwPRF = new PrintWriter(new FileWriter("abstraction.prf"));
00990 PrintWriter pwEL = new PrintWriter(new FileWriter("abstraction.el"));
00991 if (pwPVS == null || pwPRF == null || pwEL == null) {
00992 JOptionPane.showMessageDialog(this, "Unable to create temporary files", "Cannnot run PVS", JOptionPane.ERROR_MESSAGE);
00993 return;
00994 }
00995 if (parserObj.basic_type == sym.INT)
00996 PVS.begin_int(pwPVS);
00997 else
00998 PVS.begin_float(pwPVS);
00999 parserObj.tree.print_PVS(pwPVS);
01000 PVS.check(pwPVS, parserObj.npredicates);
01001 PVS.rest(pwPVS, parserObj.npredicates, parserObj.basic_type);
01002 PVS.prf(pwPRF, parserObj.npredicates, parserObj.basic_type);
01003 pwEL.println("(prove-pvs-file \"abstraction\")");
01004 pwPRF.close();
01005 pwPVS.close();
01006 pwEL.close();
01007 PVS.execAndWait("pvs -batch -q -l abstraction.el -v 1");
01008 StringWriter sw = new StringWriter();
01009 PrintWriter pwSpec = new PrintWriter(sw);
01010 if (parserObj.basic_type == sym.INT)
01011 pwSpec.print("abstraction " + parserObj.name + " extends integral\n begin\n");
01012 else
01013 pwSpec.print("abstraction " + parserObj.name + " extends real\n begin\n");
01014 pwSpec.print(" TOKENS = { ");
01015 for (int i = 0; i < parserObj.npredicates - 1; i++)
01016 pwSpec.print(parserObj.tokens.elementAt(i) + " , ");
01017 pwSpec.print(parserObj.tokens.elementAt(parserObj.npredicates - 1) + " }; ");
01018 PVS.check_BASL(pwSpec, parserObj.npredicates, parserObj.tokens);
01019 pwSpec.print("\n\n abstract(" + parserObj.variable + ")\n begin\n");
01020 parserObj.tree.print_BASL(pwSpec);
01021 pwSpec.print(" end\n\n");
01022 PVS.rest_BASL(pwSpec, parserObj.npredicates, parserObj.basic_type, parserObj.tokens);
01023 getBASLCodeTextArea().setText(sw.toString());
01024 pwSpec.close();
01025 } catch (Throwable e) {
01026 JOptionPane.showMessageDialog(this, e.getMessage(), "Cannnot run PVS", JOptionPane.ERROR_MESSAGE);
01027 e.printStackTrace();
01028 }
01029 new File("abstraction.pvs").delete();
01030 new File("abstraction.prf").delete();
01031 new File("abstraction.el").delete();
01032 }
01033 /**
01034 * Comment
01035 */
01036 public void removeButton_ActionEvents() {
01037 int index = getScrollPaneTable().getSelectedRow();
01038 if (index >= 0) {
01039 String name = (String) abstractions.toArray()[index];
01040 boolean t = "".equals(abstractionPackage) ? name.startsWith(abstractionPackage + "integral.") : name.startsWith(abstractionPackage + ".");
01041 if (t) {
01042 if (JOptionPane.showConfirmDialog(this, "Do you want to delete the Java source and class files also?", "Question", JOptionPane.YES_NO_OPTION) == JOptionPane.YES_OPTION) {
01043 AbstractionClassLoader.removeClass(name);
01044
01045 String filename = "".equals(abstractionPackage) ? abstractionPath + File.separator + name.replace('.', File.separatorChar) : abstractionPath + File.separator + name.substring(name.indexOf(abstractionPackage) + 1).replace('.', File.separatorChar);
01046 new File(filename + ".java").delete();
01047 new File(filename + ".class").delete();
01048 }
01049 }
01050 abstractions.remove(name);
01051 try {
01052 updateAbstractionList();
01053 } catch (Exception e) {
01054 }
01055 }
01056 }
01057 private void runJavac(String classpath, String filename) {
01058 String cmdLine = "javac -g -classpath " + classpath + " " + filename;
01059 System.out.println(cmdLine);
01060 sun.tools.javac.Main javac = new sun.tools.javac.Main(System.out, "Bandera");
01061 if (!javac.compile(new String[] { "-g", "-classpath", classpath, filename })) {
01062 System.out.println("Error while compiling the abstraction definition");
01063 }
01064 }
01065 /**
01066 * Comment
01067 */
01068 public void saveAsButton_ActionEvents() {
01069 FileChooser.chooser.setCurrentDirectory(new File(System.getProperty("user.dir")));
01070 FileChooser.chooser.setFileFilter(FileChooser.BASL);
01071 FileChooser.chooser.setSelectedFile(new File(""));
01072 FileChooser.chooser.setFileSelectionMode(FileChooser.FILES_ONLY);
01073 if (FileChooser.chooser.showSaveDialog(this) == FileChooser.APPROVE_OPTION) {
01074 File file = FileChooser.chooser.getSelectedFile();
01075 if (file.exists()) {
01076 if (JOptionPane.showConfirmDialog(this, "Do you want to overwrite the file?", "Confirm", JOptionPane.OK_CANCEL_OPTION) == JOptionPane.OK_OPTION) {
01077 file.delete();
01078 } else {
01079 return;
01080 }
01081 }
01082 try {
01083 PrintWriter pw = new PrintWriter(new FileWriter(file));
01084 pw.print(getBASLCodeTextArea().getText());
01085 pw.flush();
01086 pw.close();
01087 } catch (Exception e) {
01088 JOptionPane.showMessageDialog(this, e.getMessage(), "Saving Error", JOptionPane.ERROR_MESSAGE);
01089 }
01090 }
01091 }
01092 /**
01093 * Comment
01094 */
01095 public void showButton_ActionEvents() {
01096 int index = getScrollPaneTable().getSelectedRow();
01097 if (index >= 0) {
01098 getBASLCodeTextArea().setText((String) AbstractionClassLoader.invokeMethod((String) abstractions.toArray()[index], "getBASLRepresentation", new Class[0], null, new Object[0]));
01099 }
01100 }
01101 /**
01102 *
01103 */
01104 private synchronized void updateAbstractionList() throws Exception {
01105 File f = new File(abstractionListPath);
01106 if (f.exists()) f.delete();
01107 PrintWriter pw = new PrintWriter(new FileWriter(abstractionListPath));
01108 for (Iterator i = abstractions.iterator(); i.hasNext();) {
01109 pw.println(i.next().toString());
01110 }
01111 pw.flush();
01112 pw.close();
01113 updateAbstractionTable();
01114 }
01115 /**
01116 *
01117 */
01118 private void updateAbstractionTable() {
01119 JTreeTable.processAbstractions(getAbstractions());
01120 if (TypeGUI.typeGUI != null) TypeGUI.typeGUI.reset();
01121 Object[][] data = new Object[abstractions.size()][3];
01122 String[] abstractions = new String[data.length];
01123 System.arraycopy(this.abstractions.toArray(), 0, abstractions, 0, data.length);
01124 for (int i = 0; i < data.length; i++) {
01125 data[i][0] = AbstractionClassLoader.invokeMethod(abstractions[i], "getName", new Class[0], null, new Object[0]);
01126 int numTokens = ((Integer) AbstractionClassLoader.invokeMethod(abstractions[i], "getNumOfTokens", new Class[0], null, new Object[0])).intValue();
01127 HashSet tokens = new HashSet();
01128 for (int j = 0; j < numTokens; j++) {
01129 String token = (String) AbstractionClassLoader.invokeMethod(abstractions[i], "getToken", new Class[] {int.class}, null, new Object[] {new Integer(j)});
01130 tokens.add(token.substring(token.indexOf(".") + 1));
01131 }
01132 data[i][1] = tokens.toString().replace('[', '{').replace(']', '}');
01133 data[i][2] = "integral";
01134 }
01135 getScrollPaneTable().setModel(new DefaultTableModel(data, columnNames));
01136 getScrollPaneTable().sizeColumnsToFit(0);
01137 }
01138 }
1.2.10 written by Dimitri van Heesch,
© 1997-2001