src/tests/gov/nasa/jpf/util/event/EventTreeTest.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.util.event;
  20
  21 import gov.nasa.jpf.util.event.EventTree;
  22 import gov.nasa.jpf.util.event.Event;
  23 import gov.nasa.jpf.util.test.TestJPF;
  24 import org.junit.Test;
  25
  26 /**
  27  * regression test for EventTree
  28  */
  29 public class EventTreeTest extends TestJPF {
  30
  31   protected boolean checkGeneratedPaths (EventTree m, String[] expected){
  32     System.out.println("event tree: ");
  33     m.printTree();
  34
  35     int nMatches = 0;
  36     for (Event ee : m.visibleEndEvents()){
  37       String trace = ee.getPathString(null);
  38       System.out.print("checking path: \"" + trace + '"');
  39
  40       if (!m.checkPath(ee, expected)){
  41         System.out.println("   UNEXPECTED");
  42         return false;
  43       } else {
  44         System.out.println("   OK");
  45       }
  46
  47       nMatches++;
  48     }
  49
  50     if (nMatches != expected.length){
  51       System.out.println("UNCOVERED PATH: ");
  52       for (int i=0; i<expected.length; i++){
  53         if (expected[i] != null){
  54           System.err.println(expected[i]);
  55         }
  56       }
  57       return false;
  58     }
  59
  60     return true;
  61   }
  62
  63
  64   //--------------------------------------------------------------------
  65
  66   static class SimpleTree extends EventTree {
  67     @Override
  68     public Event createRoot() {
  69       return
  70         sequence(
  71           event("a"),
  72           alternatives(
  73             event("1"),
  74             iteration(2,
  75               event("x")
  76             )
  77           ),
  78           event("b")
  79         );
  80     }
  81   }
  82
  83   @Test
  84   public void testSimpleTree(){
  85     SimpleTree m = new SimpleTree();
  86
  87     String[] expected = {
  88         "a1b",
  89         "axxb"
  90     };
  91
  92     if (!checkGeneratedPaths(m, expected)){
  93       fail("failed to match traces");
  94     }
  95   }
  96
  97   //--------------------------------------------------------------------
  98   public static class CombinationTree extends EventTree {
  99     @Override
 100     public Event createRoot() {
 101       return anyCombination(
 102                event("a"),
 103                event("b"),
 104                event("c"),
 105                event("d")
 106              );
 107     }
 108   }
 109
 110   @Test
 111   public void testCombinationTree(){
 112     CombinationTree t = new CombinationTree();
 113     //t.printPaths();
 114
 115     String[] expected = {
 116         "",
 117         "a",
 118         "b",
 119         "ab",
 120         "c",
 121         "ac",
 122         "bc",
 123         "abc",
 124         "d",
 125         "ad",
 126         "bd",
 127         "abd",
 128         "cd",
 129         "acd",
 130         "bcd",
 131         "abcd"
 132     };
 133
 134     if (!checkGeneratedPaths(t, expected)){
 135       fail("failed to match traces");
 136     }
 137   }
 138
 139   static class SimpleCombinationTree extends EventTree {
 140     @Override
 141     public Event createRoot() {
 142       return anyCombination(
 143                event("a"),
 144                event("b")
 145              );
 146     }
 147   }
 148
 149   //@Test
 150   public void testSimpleCombinationTree(){
 151     SimpleCombinationTree t = new SimpleCombinationTree();
 152     System.out.println("--- tree:");
 153     t.printTree();
 154     System.out.println("--- paths:");
 155     t.printPaths();
 156   }
 157
 158   //--------------------------------------------------------------------
 159
 160   static class EmbeddedCombinationTree extends EventTree {
 161     @Override
 162     public Event createRoot() {
 163       return sequence(
 164                 event("1"),
 165                 anyCombination(
 166                    event("a"),
 167                    event("b")),
 168                 event("2"));
 169     }
 170   }
 171
 172   //@Test
 173   public void testEmbeddedCombinationTree(){
 174     EventTree t = new EmbeddedCombinationTree();
 175     System.out.println("--- tree:");
 176     t.printTree();
 177     System.out.println("--- paths:");
 178     t.printPaths();
 179   }
 180
 181
 182   //--------------------------------------------------------------------
 183   static class DT extends EventTree {
 184     @Override
 185     public Event createRoot() {
 186       return sequence(
 187               event("a"),
 188               alternatives(
 189                   event("1"),
 190                   sequence(
 191                       event("X"),
 192                       event("Y")
 193                   ),
 194                   iteration(3,
 195                       event("r")
 196                   )
 197               ),
 198               event("b"));
 199     }
 200   }
 201
 202
 203   @Test
 204   public void testMaxDepth(){
 205     DT t = new DT();
 206     t.printTree();
 207     t.printPaths();
 208
 209     int maxDepth = t.getMaxDepth();
 210     System.out.println("max depth: " + maxDepth);
 211
 212     assertTrue( maxDepth == 5);
 213   }
 214
 215   //--------------------------------------------------------------------
 216   static class PermutationTree extends EventTree {
 217     @Override
 218     public Event createRoot(){
 219       return anyPermutation(
 220                event("a"),
 221                event("b"),
 222                event("c")
 223               );
 224     }
 225   }
 226
 227   @Test
 228   public void testPermutationTree(){
 229     PermutationTree t = new PermutationTree();
 230     //t.printPaths();
 231
 232     String[] expected = {
 233         "abc",
 234         "acb",
 235         "bac",
 236         "bca",
 237         "cab",
 238         "cba"
 239       };
 240
 241     if (!checkGeneratedPaths(t, expected)){
 242       fail("failed to match traces");
 243     }
 244   }
 245
 246   //--------------------------------------------------------------------
 247   static class AddPathTree extends EventTree {
 248     @Override
 249     public Event createRoot(){
 250       return sequence(
 251                event("a"),
 252                event("b"),
 253                event("c")
 254               );
 255     }
 256   }
 257
 258   @Test
 259   public void testAddPath () {
 260     AddPathTree t = new AddPathTree();
 261     t.addPath(
 262             new Event("a"),
 263             new Event("b"),
 264             new Event("3"));
 265
 266     String[] expected = { "abc", "ab3" };
 267
 268     if (!checkGeneratedPaths(t, expected)){
 269       fail("failed to match traces");
 270     }
 271   }
 272
 273   //-------------------------------------------------------------------
 274   static class MT1 extends EventTree {
 275     @Override
 276     public Event createRoot(){
 277       return sequence(
 278                event("a"),
 279                event("b"),
 280                event("c")
 281               );
 282     }
 283   }
 284
 285   static class MT2 extends EventTree {
 286     @Override
 287     public Event createRoot(){
 288       return sequence(
 289                event("1"),
 290                event("2"),
 291                event("3")
 292               );
 293     }
 294   }
 295
 296   static class MT3 extends EventTree {
 297     @Override
 298     public Event createRoot(){
 299       return sequence(
 300                event("X"),
 301                event("Y")
 302               );
 303     }
 304   }
 305
 306
 307   @Test
 308   public void testMerge (){
 309     MT1 t1 = new MT1();
 310     MT2 t2 = new MT2();
 311     //MT3 t3 = new MT3();
 312
 313     EventTree t = t1.interleave( t2);
 314     // t.printPaths();
 315
 316     String[] expected = {
 317       "a123bc",
 318       "a12b3c",
 319       "a12bc3",
 320       "a1b23c",
 321       "a1b2c3",
 322       "a1bc23",
 323       "ab123c",
 324       "ab12c3",
 325       "ab1c23",
 326       "abc123",
 327       "123abc",
 328       "12a3bc",
 329       "12ab3c",
 330       "12abc3",
 331       "1a23bc",
 332       "1a2b3c",
 333       "1a2bc3",
 334       "1ab23c",
 335       "1ab2c3",
 336       "1abc23"
 337     };
 338
 339     if (!checkGeneratedPaths(t, expected)){
 340       fail("failed to match traces");
 341     }
 342   }
 343
 344   //-------------------------------------------------------------------
 345   static class SMT1 extends EventTree {
 346     @Override
 347     public Event createRoot(){
 348       return sequence(
 349                event("a"),
 350                event("b")
 351               );
 352     }
 353   }
 354
 355   static class SMT2 extends EventTree {
 356     @Override
 357     public Event createRoot(){
 358       return sequence(
 359                event("1"),
 360                event("2")
 361               );
 362     }
 363   }
 364
 365   //@Test
 366   public void testSimpleMerge (){
 367     SMT1 t1 = new SMT1();
 368     SMT2 t2 = new SMT2();
 369     //MT3 t3 = new MT3();
 370
 371     EventTree t = t1.interleave( t2);
 372     System.out.println("--- merged tree:");
 373     t.printTree();
 374     System.out.println("--- merged paths:");
 375     t.printPaths();
 376   }
 377
 378
 379   //-------------------------------------------------------------------
 380   static class RT1 extends EventTree {
 381     @Override
 382     public Event createRoot(){
 383       return sequence(
 384                event("a"),
 385                event("b")
 386               );
 387     }
 388   }
 389
 390   static class RT2 extends EventTree {
 391     @Override
 392     public Event createRoot(){
 393       return sequence(
 394                event("1"),
 395                event("2")
 396               );
 397     }
 398   }
 399
 400
 401   @Test
 402   public void testRemove (){
 403     RT1 t1 = new RT1();
 404     RT2 t2 = new RT2();
 405
 406     EventTree t = t1.interleave( t2);
 407     System.out.println("merged tree: ");
 408     //t.printTree();
 409     t.printPaths();
 410
 411     t = new EventTree( t.removeSource(t2));
 412     System.out.println("reduced tree: ");
 413     //t.printTree();
 414     //t.printPaths();
 415
 416     String[] expected = { "ab" };
 417     if (!checkGeneratedPaths(t, expected)){
 418       fail("failed to match traces");
 419     }
 420   }
 421 }