mc.hh 6.04 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
// Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#pragma once

Etienne Renault's avatar
Etienne Renault committed
22 23
#include <iostream>
#include <stdexcept>
24 25
#include <string>
#include <vector>
26
#include <utility>
27

Etienne Renault's avatar
Etienne Renault committed
28 29
#include <spot/misc/common.hh>

30 31
namespace spot
{
32
  /// \brief The list of parallel model-checking algorithms available
Etienne Renault's avatar
Etienne Renault committed
33
  enum class SPOT_API mc_algorithm
34 35 36 37 38
    {
     BLOEMEN_EC,    ///< \brief Bloemen.16.hvc emptiness check
     BLOEMEN_SCC,   ///< \brief Bloemen.16.ppopp SCC computation
     CNDFS,         ///< \brief Evangelista.12.atva emptiness check
     DEADLOCK,      ///< \brief Check wether there is a deadlock
39 40
     REACHABILITY,  ///< \brief Only perform a reachability algorithm
     SWARMING,      ///< \brief Holzmann.11.ieee applied to renault.13.lpar
41 42
    };

Etienne Renault's avatar
Etienne Renault committed
43
  enum class SPOT_API mc_rvalue
44 45 46 47 48 49 50 51 52 53 54 55
    {
     DEADLOCK,                  ///< \brief A deadlock has been found
     EMPTY,                     ///< \brief The product is empty
     FAILURE,                    ///< \brief The Algorithm finished abnormally
     NO_DEADLOCK,               ///< \brief No deadlock has been found
     NOT_EMPTY,                 ///< \brief The product is not empty
     SUCCESS,                   ///< \brief The Algorithm finished normally
    };

  /// \brief This structure contains, for each thread, the collected information
  /// during the traversal
  struct SPOT_API ec_stats
56
  {
57 58 59 60 61 62
   std::vector<std::string> name;     ///< \brief The name of the algorithm used
   std::vector<unsigned> walltime;    ///< \brief Walltime for this thread in ms
   std::vector<unsigned> states;      ///< \brief Number of states visited
   std::vector<unsigned> transitions; ///< \brief Number of transitions visited
   std::vector<int> sccs;             ///< \brief Number of SCCs or -1
   std::vector<mc_rvalue> value;      ///< \brief The return status
63
   std::vector<bool> finisher;        ///< \brief Is it the finisher thread?
64 65 66 67
   std::string trace;                 ///< \brief The output trace
  };

  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma)
68
  {
69
    switch (ma)
70
      {
71 72 73 74 75 76 77 78
      case mc_algorithm::BLOEMEN_EC:
        os << "bloemen_ec";  break;
      case mc_algorithm::BLOEMEN_SCC:
        os << "bloemen_scc";  break;
      case mc_algorithm::CNDFS:
        os << "cndfs";  break;
      case mc_algorithm::DEADLOCK:
        os << "deadlock";  break;
79 80
      case mc_algorithm::REACHABILITY:
        os << "reachability";  break;
81 82
      case mc_algorithm::SWARMING:
        os << "swarming";  break;
83
      }
84
    return os;
85
  }
86

87
  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr)
88
  {
89
    switch (mr)
90
      {
91 92 93 94 95 96 97 98 99 100 101 102
      case mc_rvalue::DEADLOCK:
        os << "deadlock";  break;
      case mc_rvalue::EMPTY:
        os << "empty"; break;
      case mc_rvalue::FAILURE:
        os << "failure";  break;
      case mc_rvalue::NO_DEADLOCK:
        os << "no_deadlock"; break;
      case mc_rvalue::NOT_EMPTY:
        os << "not_empty";  break;
      case mc_rvalue::SUCCESS:
        os << "success"; break;
103
      }
104
    return os;
105
  }
Antoine Martin's avatar
Antoine Martin committed
106

107
  SPOT_API std::ostream& operator<<(std::ostream& os, const ec_stats& es)
Antoine Martin's avatar
Antoine Martin committed
108
  {
109
    for (unsigned i = 0; i < es.name.size(); ++i)
Antoine Martin's avatar
Antoine Martin committed
110
      {
111 112 113 114 115
        os << "---- Thread number:\t" << i << '\n'
           << "   - Algorithm:\t\t" << es.name[i] << '\n'
           << "   - Walltime (ms):\t" << es.walltime[i] <<'\n'
           << "   - States:\t\t" << es.states[i] << '\n'
           << "   - Transitions:\t" << es.transitions[i] << '\n'
116 117
           << "   - Result:\t\t" << es.value[i] << '\n'
           << "   - SCCs:\t\t" << es.sccs[i] << '\n';
118

119 120
        os << "CSV: tid,algorithm,walltime,states,transitions,"
              "sccs,result,finisher\n"
121 122
           << "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ','
           << es.states[i] << ',' << es.transitions[i] << ','
123 124
           << es.sccs[i] << ',' << es.value[i]
           << ',' << es.finisher[i] << "\n\n";
Antoine Martin's avatar
Antoine Martin committed
125
      }
126
    return os;
Antoine Martin's avatar
Antoine Martin committed
127
  }
Antoine Martin's avatar
Antoine Martin committed
128

129 130 131
  /// \brief This function helps to find the output value from a set of threads
  /// that may have different values.
  SPOT_API const mc_rvalue operator|(const mc_rvalue& lhs, const mc_rvalue& rhs)
Antoine Martin's avatar
Antoine Martin committed
132
  {
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
    // Handle Deadlocks
    if (lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::DEADLOCK)
      return mc_rvalue::DEADLOCK;
    if (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK)
      return mc_rvalue::NO_DEADLOCK;
    if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) ||
        (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::DEADLOCK))
      return mc_rvalue::DEADLOCK;

    // Handle Emptiness
    if (lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::EMPTY)
      return mc_rvalue::EMPTY;
    if (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::NOT_EMPTY)
      return mc_rvalue::NOT_EMPTY;
    if ((lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::NOT_EMPTY) ||
        (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::EMPTY))
      return mc_rvalue::EMPTY;

    // Handle Failure / Success
    if (lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::FAILURE)
      return mc_rvalue::FAILURE;
    if (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::SUCCESS)
      return mc_rvalue::SUCCESS;
    if ((lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::SUCCESS) ||
        (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::FAILURE))
      return mc_rvalue::FAILURE;

    throw std::runtime_error("Unable to compare these elements!");
Antoine Martin's avatar
Antoine Martin committed
161
  }
162
}