Java > Open Source Codes > SOFA > SOFAnode > Util > checker


1 /* $Id: checker.java,v 1.2 2004/05/20 14:23:53 bures Exp $ */
2
3 package SOFA.SOFAnode.Util;
4
5 import java.io.BufferedReader ;
6 import java.io.FileReader ;
7 import java.io.IOException ;
8 import java.io.Reader ;
9 import java.util.Collection ;
10 import java.util.Iterator ;
11 import java.util.LinkedList ;
12
13
14 /**
15  * An implementation class for protocol inclusion checker.
16  *
17  * @author Stanislav Visnovsky
18  * @version 2.0.0
19  * @see Builder
20  * @see Machine
21 */
22 public class checker implements BehaviorProtocolChecker {
23
24 /**
25  * String containing the first protocol.
26 */
27     private static String protocol1 = null;
28
29 /**
30  * String containing the second protocol.
31 */
32     private static String protocol2 = null;
33
34 /**
35  * A reference to a set, which contains the action tokens of the external set.
36 */
37     private static String external[];
38
39 /**
40  * A reference to a set, which contains the action tokens of all interface events for frame to architecture.
41 */
42     private static String all[];
43
44 /**
45  * Whether to run the conformance test. Used by the {@link checker#parseArguments} to inform
46  * {@link checker#main} in case of --version and --help arguments.
47 */
48     private static boolean dontrun = false;
49     private static int test = -1;
50
51     public checker() {
52     EdgeFactory.initActionTokens();
53     }
54 /**
55  * The main entry point of the standalone invocation of checker class. The arguments passed
56  * from the command line are filenames which contain protocols. Optionally an user can
57  * specify the external set. The arguments are parsed by the method parseArguments.
58  * Then, the conformance is tested via int2frame and frame2arch methods.
59  * The result is printed on the standard output.
60  *
61  * @author Stanislav Visnovsky
62  * @version 2.0.0
63  *
64  * @param args parameters passed from the command line.
65  * @throws SyntaxErrorException in case of syntactic error of the specified protocols or sets
66  * @throws IOException if there are problems with reading the specified files
67  * @see checker#parseArguments
68  * @see checker#int2frame
69  * @see checker#frame2arch
70  *
71 */
72     public static void main(String [] args) throws SyntaxErrorException, IOException {
73
74     Debug.debug = Integer.parseInt( System.getProperty( "ProtocolDebug","0"));
75
76     String result = null;
77     
78       try {
79         checker check = new checker();
80
81         parseArguments( args );
82         if( dontrun ) return;
83
84     long time = System.currentTimeMillis();
85         switch( test ) {
86             case 0: result = check.int2frame(protocol1,true,external,protocol2); break;
87             case 1: result = check.int2frame(protocol1,false,external,protocol2); break;
88             case 2: result = check.frame2arch(protocol1,external,protocol2,all); break;
89             case 3: result = check.int2int(protocol1,external,protocol2); break;
90             default: System.out.println( "Unknown conformance test"); return;
91         }
92
93         System.out.print("1st conforms to 2nd:");
94         if( result == null ) System.err.println("yes");
95         else System.err.println("no - "+result);
96
97     System.out.println("Statistics:");
98     System.out.println("Maximal number of states:"+machineImpl.maxstates );
99     Debug.println(1,"Time:"+((System.currentTimeMillis() - time)/1000) );
100       } catch (java.lang.Exception e) { System.out.println("caught "+e); e.printStackTrace(); };
101
102     }
103
104 /**
105  * Parses the arguments from the command line. For version and help options prints the corresponding
106  * information. If there is debug option present, it sets the Debug.debug flag to 1 to allow
107  * the printing of the debugging information to standard output. If the restricting sets are
108  * specified, they are parsed and the instances of the TreeSet class are created. In case
109  * of syntax error, the SyntaxErrorException is raised.
110  *
111  * @author Stanislav Visnovsky
112  * @version 1.0.0
113  *
114  * @throws SyntaxErrorException in case of syntactic error of the specified protocols or sets
115  * @throws IOException if there are problems with reading the specified files
116  * @see checker#main
117  * @see checker#printHelp
118  * @see checker#protocol1
119  * @see checker#protocol2
120  * @see checker#external
121  * @see checker#all
122  * @see Debug
123  *
124 */
125     private static void parseArguments( String [] args ) throws SyntaxErrorException, IOException {
126     int i;
127
128     String s1 = null;
129     String s2 = null;
130
131     for( i = 0; i< args.length; i++ ) {
132         if( args[i].compareTo( "--debug" ) == 0 ) Debug.debug = 1;
133         else if( args[i].compareTo( "--version") == 0 ) {
134         System.out.println("Behavior protocol verifier v2.1");
135         dontrun = true;
136         return;
137         } else if( args[i].compareTo( "--help" ) == 0 ) {
138         printHelp();
139         dontrun = true;
140         return;
141         } else if( args[i].compareTo( "-t" ) == 0 ) {
142             i++;
143             if( i == args.length ) throw new SyntaxErrorException( "conformance type expected");
144             try {
145                 test = Integer.parseInt(args[i]);
146             } catch( NumberFormatException e ) {
147                 throw new SyntaxErrorException( "conformance type has to be 0-3");
148             }
149             if( test<0 || test>3 ) throw new SyntaxErrorException( "conformance type has to be 0-3");
150         } else if (args[i].compareTo( "--file") == 0 ) {
151           if ( i == args.length ) throw new SyntaxErrorException( "protocol filename expected");
152           i++;
153           BufferedReader br = new java.io.BufferedReader ( new java.io.FileReader (args[i]));
154           StringBuffer sb = new StringBuffer ();
155           String st;
156           while ((st=br.readLine())!=null) { sb.append(st); };
157           String protdata = sb.toString();
158           /* new java.io.BufferedReader( new java.io.FileReader(args[i])).readLine(); */
159           if ( protocol1 == null) protocol1 = protdata;
160           else if (protocol2 == null) protocol2 = protdata;
161           else throw new SyntaxErrorException( "too many --file arguments");
162         } else
163           if( protocol1 == null ) protocol1 = args[i];
164          else if( protocol2 == null ) protocol2 = args[i];
165               else if( s1 == null ) s1 = args[i];
166                 else if( s2 == null ) s2 = args[i];
167                     else { printHelp(); throw new SyntaxErrorException("Too much arguments") ; }
168     }
169
170     if( protocol1 == null || protocol2 == null ) {
171         printHelp();
172         throw new SyntaxErrorException("Not enough arguments");
173     }
174
175     Collection extern = new LinkedList ();
176
177     if( s1 != null ) {
178
179         Reader source = new FileReader ( s1 );
180         while( source.ready() ) {
181         String event = "";
182         char ch;
183         do {
184             ch = (char)source.read();
185             if( ch != ',') event = event + ch;
186         } while( ch != ',' && source.ready() );
187         if( event.length() > 0 ) {
188             extern.add( event );
189             ActionToken t = new ActionToken( event );
190             Debug.println(3, "Looking up "+t.name );
191             EdgeFactory.getActionTokenIdx( t );
192         }
193         }
194     }
195
196     external = new String [ extern.size() ];
197     int id = 0;
198     for( Iterator it = extern.iterator(); it.hasNext(); )
199     external[id++] = (String )it.next();
200
201     Collection al = new LinkedList ();
202
203     if( s2 != null ) {
204
205         Reader source = new FileReader ( s2 );
206         while( source.ready() ) {
207         String event = "";
208         char ch;
209         do {
210             ch = (char)source.read();
211             if( ch != ',') event = event + ch;
212         } while( ch != ',' && source.ready() );
213         if( event.length() > 0 ) {
214             al.add( event );
215             ActionToken t = new ActionToken(event);
216             EdgeFactory.getActionTokenIdx( t );
217         }
218         }
219     }
220
221     all = new String [ al.size() ];
222     id = 0;
223     for( Iterator it = al.iterator(); it.hasNext(); )
224     all[id++] = (String )it.next();
225
226     if( Debug.debug == 0 ) Debug.debug = Integer.parseInt( System.getProperty( "ProtocolDebug","0"));
227
228     Debug.println("Command line arguments:");
229     Debug.println("Protocol 1: "+protocol1 );
230     Debug.println("Protocol 2: "+protocol2 );
231     Debug.println("Conformance type: "+test );
232     Debug.println("Debug: " + Debug.debug );
233     Debug.print("External: " );
234     for( id = 0; id < external.length; id++)
235         Debug.print( external[id]+", ");
236     Debug.println();
237 // Debug.println("All (for type 2): "+all.toList() );
238 }
239
240 /**
241  * Prints the help for invoking the checker by its main method.
242  *
243  * @author Stanislav Visnovsky
244  * @version 1.0.0
245  *
246  * @see checker#main
247  *
248 */
249     private static void printHelp() {
250     System.out.println("Behavior protocol verifier v2.1");
251     System.out.println("usage: java SOFA.SOFAnode.Util.checker -t <type>[--debug] protocol1 protocol2 [external]");
252     System.out.println(" java SOFA.SOFAnode.Util.checker --version");
253     System.out.println(" java SOFA.SOFAnode.Util.checker --help");
254     System.out.println();
255     System.out.println("where <type> is:");
256     System.out.println("0 for provides interface protocol vs frame protocol");
257     System.out.println("1 for requires interface protocol vs frame protocol");
258     System.out.println("2 for frame protocol vs architecture protocol");
259     System.out.println("3 for interface protocol vs interface protocol");
260     }
261
262 /**
263  * Checks, whether the protocols passed as arguments generate language that are in
264  * inclusion, i.e., L(PA) is a subset of L(PB).
265  * Before the inclusion homomorphism lookup, there must be the reduction performed.
266  *
267  * @author Stanislav Visnovsky
268  * @version 2.5.0
269  *
270  * @param mA the first protocol
271  * @param mB the second protocol
272  * @return result of the inclusion test, null for success, counterexample otherwise
273  * @see checker#main
274  * @see Machine#Reduce
275  * @see Machine#Determinize
276  * @see Machine#Reachable
277  * @see Machine#isIncludedIn
278  *
279 */
280     private static String inclusion( Protocol A, Protocol B ) throws SyntaxErrorException
281     {
282
283     Builder builder = new Builder();
284     
285         Debug.println(1,"Start of inclusion testing");
286         
287     A = distributeRepetition( A );
288     B = distributeRepetition( B );
289     
290     Debug.println(1,"Heuristics done" );
291     Debug.println(2,"Left protocol:");
292     ((Printer)A).Print( 2 );
293     Debug.println(2,"Right protocol:");
294     ((Printer)B).Print( 2 );
295     
296     long time = System.currentTimeMillis();
297
298     Protocol PmA = A.Copy() ;
299
300     Machine mA = PmA.createMachine();
301     Debug.println(1,"inclusion left (A) machine:");
302     ((Printer)mA).Print(2);
303
304     System.gc();
305     
306     Machine mBc1 = B.createMachine();
307     Debug.println(1,"inclusion right (B) machine:");
308     ((Printer)mBc1).Print(2);
309
310     System.gc();
311     
312         Debug.println(1, "Time for building: "+ (System.currentTimeMillis()-time));
313
314         // lookup inclusion
315 time = System.currentTimeMillis();
316         Debug.println(1,"Inclusion lookup:");
317         String result = mA.isIncludedIn( mBc1 );
318         Debug.println(1, "Time for inclusion lookup: "+ ((System.currentTimeMillis()-time)/1000)+"s");
319
320     return result;
321     }
322
323 /**
324  * Checks, whether the protocol1 can be updated by protocol 2
325  *
326  * @author Stanislav Visnovsky
327  * @version 1.0.0
328  *
329  * @param protocol1 the first protocol
330  * @param protocol2 the second protocol
331  * @param external a set of event tokens to be evaluated
332  * @param provision a set of event tokens to be considered as provision alphabet
333  * @return result of the inclusion test, null for success, counterexample otherwise
334 */
335   public String canAlwaysUpdate( Protocol protocol1, Protocol protocol2, ActionTokenArray external, ActionTokenArray provision)
336     throws SyntaxErrorException
337   {
338     Debug.println(1,"Start of canAlwaysUpdate" );
339
340     // condition 1
341
342     Protocol leftproto = protocol2.Copy();
343
344     leftproto.Restrict( new ActionTokenArray( provision ) );
345     leftproto = new ProtocolRestriction( leftproto, provision );
346     
347     Debug.println(2, "Left of condition 1 restricted to "+provision.toList()+":" );
348     leftproto.Print( 2 );
349     
350     Protocol rightproto = new ProtocolUpdateStripped( protocol2.Copy() ) ;
351     rightproto = new ProtocolSequence( rightproto, protocol1.Copy() );
352
353     rightproto.Restrict( new ActionTokenArray( provision ) );
354     rightproto = new ProtocolRestriction( rightproto, provision );
355     
356     Debug.println(2, "Right of condition 1 restricted:" );
357     rightproto.Print( 2 );
358     
359     String result = inclusion( leftproto,rightproto );
360     if( result != null) return "Condition 1 violated:"+result;
361
362     //condition 2
363
364     Protocol pom = new ProtocolUpdateStripped( protocol2.Copy() ) ;
365     pom = new ProtocolSequence( pom, protocol1.Copy() );
366     pom.Restrict( new ActionTokenArray( external ) );
367     pom = new ProtocolRestriction( pom, external );
368
369     leftproto = new ProtocolAdjustment( leftproto , pom, new ActionTokenArray(provision) ) ;
370
371     rightproto = protocol2;
372     rightproto.Restrict( new ActionTokenArray( external ) );
373     rightproto = new ProtocolRestriction( rightproto, external );
374
375     result =
376 inclusion( leftproto, rightproto ); return result == null ? null : "Condition 2 violated:"+result;
377
378   }
379
380   public String iscompliant( Protocol protocol1, Protocol protocol2, ActionTokenArray external)
381     throws SyntaxErrorException
382   {
383
384     Debug.println(1,"Start of iscomplaint" );
385
386     // condition 1
387
388     Protocol leftproto = protocol2.Copy();
389
390     leftproto.Restrict( new ActionTokenArray( external ) );
391     leftproto = new ProtocolRestriction( leftproto, external );
392     
393     Debug.println(2, "Left of condition 1 restricted to "+external.toList()+":" );
394     leftproto.Print( 2 );
395     
396     Protocol rightproto = protocol1.Copy();
397     rightproto.Restrict( new ActionTokenArray( external ) );
398     rightproto = new ProtocolRestriction( rightproto, external );
399     
400     Debug.println(2, "Right of condition 1 restricted:" );
401     rightproto.Print( 2 );
402     
403     String result = inclusion( leftproto,rightproto );
404     if( result != null) return "Condition 1 violated:"+result;
405
406     //condition 2
407
408     leftproto = new ProtocolAdjustment( leftproto , protocol1, new ActionTokenArray(external) ) ;
409     rightproto = protocol2;
410
411     result =
412 inclusion( leftproto, rightproto ); return result == null ? null : "Condition 2 violated:"+result;
413   }
414
415 /**
416  * Checks the conformance relation between interface protocol and frame protocol.
417  * This is done by preparing correct arguments for the iscompliant method, which
418  * is used to determine the result (an error message or null for success).
419  * This method works for both provides and requires protocols.
420  * No renaming takes place. Implemented by invoking the method with the same name
421  * but with an ActionTokenArray as a set of external events.
422  *
423  * @author Stanislav Visnovsky
424  * @version 1.0.0
425  *
426  * @return null for successufull test or an error message.
427  * @param ifaceProt interface protocol
428  * @param frameProt frame protocol
429  * @param ifaceOperations an array of strings for each method on the interface
430  * @param provide true for provides interface, false for requires interface
431
432  * @see checker#iscompliant
433  * @see ActionTokenArray
434  * @see checker#frame2arch
435  *
436 */
437   public String int2frame(String ifaceProt, boolean provide, String [] ifaceOperations, String frameProt)
438     throws SyntaxErrorException
439   {
440     EdgeFactory.initActionTokens();
441     Debug.debug = Integer.parseInt(System.getProperty( "ProtocolDebug","0" ));
442
443     for( int i = 0 ; i<ifaceOperations.length; i++ )
444     Builder.fillOneName( ifaceOperations[i], false );
445
446     ActionTokenArray ifaceOps = new ActionTokenArray( ifaceOperations );
447
448     String result;
449
450     Builder builder = new Builder();
451
452     builder.fillIdentifiers( ifaceProt );
453     builder.fillIdentifiers( frameProt );
454
455     Protocol iface = builder.Build( ifaceProt );
456     Protocol frame = builder.Build( frameProt );
457
458     Debug.println(3,"Restrict to:" + ifaceOps.toList() );
459     frame.Restrict( new ActionTokenArray( ifaceOps ) );
460
461     Debug.println(2,"Int2Frame restricted frame:");
462     ((Printer)frame).Print(2);
463
464         // we can ignore requirement for B(Pf), since interface cannot contain [UPDATE]
465 if( provide ) {
466             result = inclusion( iface, frame ); // this is reduced notion of protocol conformance for provides interface vs frame protocols
467 if( result == null ) return null;
468             else return "Frame protocol does not conform to provides interface protocol: Condition 1 violated: "+result;
469         } else {
470             result = inclusion( frame, iface );
471         if( result == null ) return null; // this is reduced notion of protocol conformance for requires interface vs frame protocols
472 else return "Frame protocol does not conform to requires interface protocol: Condition 2 vioated: "+result;
473         }
474   }
475
476 /**
477  * Checks the conformance relation between frame protocol and architecture protocol.
478  * This is done by preparing correct arguments for the iscompliant method, which
479  * is used to determine the result (an error message or null for success). The architecture
480  * protocol is restricted to only outer interfaces (both provides and requires).
481  * No renaming takes place.
482  *
483  * @author Stanislav Visnovsky
484  * @version 1.0.0
485  *
486  * @return null for successufull test or an error message.
487  * @param archProt architecture protocol
488  * @param frameProt frame protocol
489  * @param providesOperations an array of strings for each method on each provides interface of the frame
490  * @param ifaceOperations an array of strings for each method on each interface of the frame
491
492  * @see checker#iscompliant
493  * @see ActionTokenArray
494  * @see checker#int2frame
495  *
496 */
497   public String frame2arch(String frameProt, String [] providesOperations,
498   String archProt, String [] ifaceOperations) throws SyntaxErrorException
499   {
500     EdgeFactory.initActionTokens();
501     Debug.debug = Integer.parseInt(System.getProperty( "ProtocolDebug","0" ));
502
503     for( int i = 0 ; i<providesOperations.length; i++ )
504     Builder.fillOneName( providesOperations[i], false );
505
506     for( int i = 0 ; i<ifaceOperations.length; i++ )
507     Builder.fillOneName( ifaceOperations[i], false );
508
509     Builder builder = new Builder();
510
511     builder.fillIdentifiers( frameProt );
512     builder.fillIdentifiers( archProt );
513
514     ActionTokenArray provides = new ActionTokenArray( providesOperations );
515     ActionTokenArray iface = new ActionTokenArray(ifaceOperations);
516
517         Debug.println( 1, "Starting frame to architecture conformance" );
518
519     Debug.println( 2, "Frame protocol: "+frameProt );
520     Debug.println( 2, "Architecture protocol: "+archProt );
521     Debug.println( 2, "External events: "+provides.toList() );
522     Debug.println( 2, "All frame events: "+iface.toList() );
523
524     builder.fillIdentifiers( frameProt );
525     builder.fillIdentifiers( archProt );
526
527     Protocol frame = builder.Build( frameProt );
528     Protocol arch = builder.Build( archProt );
529     
530     arch = new ProtocolRestriction( arch, iface );
531
532     String result = iscompliant( arch, frame, provides );
533         if( result == null ) return null;
534         else return "Frame protocol does not conform to architecture protocol: "+result;
535   }
536
537 /**
538  * Checks the conformance relation between two interface protocols.
539  * This is done by preparing correct arguments for the iscompliant method, which
540  * is used to determine the result (an error message or null for success).
541  * No renaming takes place. Implemented by invoking the method with the same name
542  * but with an ActionTokenArray as a set of external events.
543  *
544  * @author Stanislav Visnovsky
545  * @version 1.0.0
546  *
547  * @return null for successufull test or an error message.
548  * @param intProt1 1st interface protocol
549  * @param intProt2 2st interface protocol
550  * @param providesOperations an array of strings for each method on an interface
551
552  * @see ActionTokenArray
553  * @see checker#int2int
554  *
555 */
556
557   public String int2int(String intProt1, String [] providesOperations, String intProt2)
558     throws SyntaxErrorException
559   {
560     EdgeFactory.initActionTokens();
561     Debug.debug = Integer.parseInt(System.getProperty( "ProtocolDebug","0" ));
562     for( int i = 0 ; i<providesOperations.length; i++ )
563     Builder.fillOneName( providesOperations[i], false );
564
565     ActionTokenArray provides = new ActionTokenArray( providesOperations );
566     throw new SyntaxErrorException( "Conformance type not supported" );
567   }
568
569   public int StatisticsMaxStates() {
570     return machineImpl.maxstates;
571   }
572
573   public void InitStatistics() {
574     machineImpl.maxstates = 0;
575   }
576
577   private static Protocol distributeRepetition( Protocol prot ) {
578     if( prot == null ) return null;
579
580     if( prot.getElement() == "*" ) {
581     Debug.println( 3, "Repetition distribution");
582     Protocol l = prot.Left();
583     if( l instanceof ProtocolOrParallel ) {
584         Protocol protl = new ProtocolRepetition( l.Left() );
585         Protocol protr = new ProtocolRepetition( l.Right() );
586         protl = distributeRepetition( protl );
587         protr = distributeRepetition( protr );
588         return new ProtocolOrParallel( protl, protr );
589     } else return new ProtocolRepetition( distributeRepetition(l) );
590     } else if( prot instanceof ProtocolToken ) {
591     return new ProtocolToken( (ActionToken)prot.getElement() );
592     } else { // if it is not repetition
593 Object protl = distributeRepetition( prot.Left() );
594     Object protr = distributeRepetition( prot.Right() );
595     return prot.getSameType( protl, protr );
596     }
597   }
598 }
599

A to Z: JavaDoc & Examples

---

Daily Java News & Articles

---

Open Source Projects

---

Open Source Codes

---

Free Computer Books

---

Remove Frame

---

Popular Tags