src/main/gov/nasa/jpf/listener/DPORStateReducer.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 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.ListenerAdapter;
  23 import gov.nasa.jpf.search.Search;
  24 import gov.nasa.jpf.jvm.bytecode.*;
  25 import gov.nasa.jpf.vm.*;
  26 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  27 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  28 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  29 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  30
  31 import java.io.PrintWriter;
  32 import java.util.*;
  33
  34 // TODO: Fix for Groovy's model-checking
  35 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
  36 /**
  37  * Simple tool to log state changes.
  38  *
  39  * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
  40  * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
  41  *
  42  * The algorithm is presented on page 11 of the paper. Basically, we create a graph G
  43  * (i.e., visible operation dependency graph)
  44  * that maps inter-related threads/sub-programs that trigger state changes.
  45  * The key to this approach is that we evaluate graph G in every iteration/recursion to
  46  * only update the backtrack sets of the threads/sub-programs that are reachable in graph G
  47  * from the currently running thread/sub-program.
  48  */
  49 public class DPORStateReducer extends ListenerAdapter {
  50
  51   // Debug info fields
  52   private boolean verboseMode;
  53   private boolean stateReductionMode;
  54   private final PrintWriter out;
  55   private String detail;
  56   private int depth;
  57   private int id;
  58   private Transition transition;
  59
  60   public DPORStateReducer(Config config, JPF jpf) {
  61     verboseMode = config.getBoolean("printout_state_transition", false);
  62     stateReductionMode = config.getBoolean("activate_state_reduction", true);
  63     if (verboseMode) {
  64       out = new PrintWriter(System.out, true);
  65     } else {
  66       out = null;
  67     }
  68   }
  69
  70   @Override
  71   public void stateRestored(Search search) {
  72     if (verboseMode) {
  73       id = search.getStateId();
  74       depth = search.getDepth();
  75       transition = search.getTransition();
  76       detail = null;
  77       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
  78               " and depth: " + depth + "\n");
  79     }
  80   }
  81
  82   @Override
  83   public void searchStarted(Search search) {
  84     if (verboseMode) {
  85       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
  86     }
  87   }
  88
  89   @Override
  90   public void stateAdvanced(Search search) {
  91     if (verboseMode) {
  92       id = search.getStateId();
  93       depth = search.getDepth();
  94       transition = search.getTransition();
  95       if (search.isNewState()) {
  96         detail = "new";
  97       } else {
  98         detail = "visited";
  99       }
 100
 101       if (search.isEndState()) {
 102         out.println("\n==> DEBUG: This is the last state!\n");
 103         detail += " end";
 104       }
 105       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 106               " which is " + detail + " Transition: " + transition + "\n");
 107     }
 108   }
 109
 110   @Override
 111   public void stateBacktracked(Search search) {
 112     if (verboseMode) {
 113       id = search.getStateId();
 114       depth = search.getDepth();
 115       transition = search.getTransition();
 116       detail = null;
 117
 118       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 119               " and depth: " + depth + "\n");
 120     }
 121   }
 122
 123   @Override
 124   public void searchFinished(Search search) {
 125     if (verboseMode) {
 126       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 127     }
 128   }
 129 }