mc.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et
// 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
 
#include <iostream>
#include <stdexcept>
#include <string>
#include <vector>
#include <utility>
 
#include <spot/misc/common.hh>
 
namespace spot
{
  enum class SPOT_API mc_algorithm
    {
     BLOEMEN_EC,    
     BLOEMEN_SCC,   
     CNDFS,         
     DEADLOCK,      
     REACHABILITY,  
     SWARMING,      
    };
 
  enum class SPOT_API mc_rvalue
    {
     DEADLOCK,                  
     EMPTY,                     
     FAILURE,                    
     NO_DEADLOCK,               
     NOT_EMPTY,                 
     SUCCESS,                   
    };
 
  struct SPOT_API ec_stats
  {
   std::vector<std::string> name;     
   std::vector<unsigned> walltime;    
   std::vector<unsigned> states;      
   std::vector<unsigned> transitions; 
   std::vector<int> sccs;             
   std::vector<mc_rvalue> value;      
   std::vector<bool> finisher;        
   std::string trace;                 
  };
 
  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma)
  {
    switch (ma)
      {
      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;
      case mc_algorithm::REACHABILITY:
        os << "reachability";  break;
      case mc_algorithm::SWARMING:
        os << "swarming";  break;
      }
    return os;
  }
 
  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr)
  {
    switch (mr)
      {
      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;
      }
    return os;
  }
 
  SPOT_API std::ostream& operator<<(std::ostream& os, const ec_stats& es)
  {
    for (unsigned i = 0; i < es.name.size(); ++i)
      {
        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'
           << "   - Result:\t\t" << es.value[i] << '\n'
           << "   - SCCs:\t\t" << es.sccs[i] << '\n';
 
        os << "CSV: tid,algorithm,walltime,states,transitions,"
              "sccs,result,finisher\n"
           << "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ','
           << es.states[i] << ',' << es.transitions[i] << ','
           << es.sccs[i] << ',' << es.value[i]
           << ',' << es.finisher[i] << "\n\n";
      }
    return os;
  }
 
  SPOT_API const mc_rvalue operator|(const mc_rvalue& lhs, const mc_rvalue& rhs)
  {
    // 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!");
  }
}