src/main/gov/nasa/jpf/listener/StateCountEstimator.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.ListenerAdapter;
  22 import gov.nasa.jpf.search.Search;
  23 import gov.nasa.jpf.vm.ChoiceGenerator;
  24 import gov.nasa.jpf.vm.VM;
  25 import gov.nasa.jpf.vm.Path;
  26 import gov.nasa.jpf.vm.Transition;
  27
  28 import java.io.PrintWriter;
  29 import java.util.Formatter;
  30
  31 /**
  32  * From already visited states, estimates the total number of states by the branching factor.
  33  */
  34
  35 public class StateCountEstimator extends ListenerAdapter
  36 {
  37    private final PrintWriter   m_out;
  38    private final StringBuilder m_buffer    = new StringBuilder();
  39    private final Formatter     m_formatter = new Formatter(m_buffer);
  40    private final int           m_logPeriod;
  41    private       double        m_lastPercent;
  42    private       long          m_nextLog;
  43    private       long          m_startTime;
  44
  45    public StateCountEstimator(Config config)
  46    {
  47       m_out       = new PrintWriter(System.out, true);
  48       m_logPeriod = config.getInt("jpf.state_count_estimator.log_period", 0);
  49    }
  50
  51    @Override
  52    public void searchStarted(Search search)
  53    {
  54       m_nextLog     = 0;
  55       m_lastPercent = 0.0;
  56       m_startTime   = System.currentTimeMillis();
  57    }
  58
  59    @Override
  60    public void searchFinished(Search search)
  61    {
  62       log(search);
  63    }
  64
  65    @Override
  66    public void stateProcessed(Search search)
  67    {
  68       if (m_nextLog > System.currentTimeMillis())
  69          return;
  70
  71       if (log(search))
  72          m_nextLog = m_logPeriod + System.currentTimeMillis();
  73    }
  74
  75    private boolean log(Search search)
  76    {
  77       VM vm;
  78       Path path;
  79       Transition trans;
  80       ChoiceGenerator cg;
  81       double percent, delta;
  82       long currentState, expectedState, currentTime, expectedTime;
  83       int i, size, processed;
  84
  85       vm       = search.getVM();
  86       path      = vm.getPath();
  87       size      = path.size();
  88       percent   = 0.0;
  89       delta     = 1.0;
  90       processed = 0;
  91
  92       for (i = 0; i < size; i++)
  93       {
  94          trans      = path.get(i);
  95          cg         = trans.getChoiceGenerator();
  96          delta     /= cg.getTotalNumberOfChoices();
  97          processed  = cg.getProcessedNumberOfChoices() - 1;
  98          percent   += delta * processed;
  99       }
 100
 101       if (size == 0)
 102          percent = 1.0;
 103
 104       if (m_lastPercent > percent)  // Sometimes a state is declared as processed but doesn't show up in the path so the percentage appears to go backwards.
 105          return(false);
 106
 107       m_lastPercent = percent;
 108
 109       currentState  = vm.getStateCount();
 110       expectedState = (long) (currentState / percent);
 111
 112       currentTime   = System.currentTimeMillis() - m_startTime;
 113       expectedTime  = (long) (currentTime / percent);
 114
 115       m_formatter.format("State:  %,d / %,d (%g%%)    Time:  ", currentState, expectedState, 100.0 * percent);
 116
 117       formatTime(expectedTime);
 118       m_buffer.append(" - ");
 119       formatTime(currentTime);
 120       m_buffer.append(" = ");
 121       formatTime(expectedTime - currentTime);
 122
 123       m_out.println(m_buffer.toString());
 124       m_buffer.setLength(0);
 125
 126       return(true);
 127    }
 128
 129    private void formatTime(long time)
 130    {
 131       long days, hours, minutes, seconds;
 132       boolean commit;
 133
 134       seconds = time / 1000;
 135       minutes = seconds / 60;
 136       hours   = minutes / 60;
 137       days    = hours / 24;
 138
 139       seconds %= 60;
 140       minutes %= 60;
 141       hours   %= 24;
 142
 143       commit = false;
 144
 145       if ((commit) || (days != 0))
 146       {
 147          commit = true;
 148          m_buffer.append(days);
 149          m_buffer.append(' ');
 150       }
 151
 152       if ((commit) || (hours != 0))
 153       {
 154          if ((commit) && (hours < 10))
 155             m_buffer.append('0');
 156
 157          m_buffer.append(hours);
 158          m_buffer.append(':');
 159          commit = true;
 160       }
 161
 162       if ((commit) || (minutes != 0))
 163       {
 164          if ((commit) && (minutes < 10))
 165             m_buffer.append('0');
 166
 167          m_buffer.append(minutes);
 168          m_buffer.append(':');
 169          commit = true;
 170       }
 171
 172       if ((commit) && (seconds < 10))
 173          m_buffer.append('0');
 174
 175       m_buffer.append(seconds);
 176    }
 177 }