text:
/*
 * Licensed to the Apache Software Foundation (ASF) under one or more
 * contributor license agreements.  See the NOTICE file distributed with
 * this work for additional information regarding copyright ownership.
 * The ASF licenses this file to You under the Apache License, Version 2.0
 * (the "License"); you may not use this file except in compliance with
 * the License.  You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

#include "util/Log.hpp"

#include <algorithm>
#include <cctype>
#include <chrono>
#include <cinttypes>
#include <ctime>
#include <mutex>
#include <string>
#include <thread>
#include <utility>
#include <vector>

#include <ace/ACE.h>
#include <ace/Dirent.h>
#include <ace/Dirent_Selector.h>
#include <ace/OS.h>
#include <ace/OS_NS_Thread.h>
#include <ace/OS_NS_sys_stat.h>
#include <ace/OS_NS_sys_time.h>
#include <ace/OS_NS_time.h>
#include <ace/OS_NS_unistd.h>
#include <boost/process/environment.hpp>

#include <geode/ExceptionTypes.hpp>
#include <geode/internal/geode_globals.hpp>
#include <geode/util/LogLevel.hpp>

#include "../internal/hacks/AceThreadId.h"
#include "geodeBanner.hpp"
#include "util/chrono/time_point.hpp"

#if defined(_WIN32)
#include <io.h>
#define GF_FILEEXISTS(x) _access_s(x, 00)
#else
#include <unistd.h>
#define GF_FILEEXISTS(x) access(x, F_OK)
#endif

/*****************************************************************************/

/**
 * The implementation of the Log class
 *
 *
 */

/*****************************************************************************/

namespace apache {
namespace geode {
namespace log {
namespace globals {

std::string* g_logFile = nullptr;
std::string* g_logFileWithExt = nullptr;

size_t g_bytesWritten = 0;
bool g_isLogFileOpened = false;

size_t g_fileSizeLimit = GEODE_MAX_LOG_FILE_LIMIT;
size_t g_diskSpaceLimit = GEODE_MAX_LOG_DISK_LIMIT;

char g_logFileNameBuffer[2048] = {0};

std::mutex g_logMutex;

int g_rollIndex = 0;
size_t g_spaceUsed = 0;
// Make a pair for the filename & its size
std::pair<std::string, int64_t> g_fileInfoPair;
// Vector to hold the fileInformation
typedef std::vector<std::pair<std::string, int64_t> > g_fileInfo;

FILE* g_log = nullptr;
ACE_utsname g_uname;
pid_t g_pid = 0;

}  // namespace globals
}  // namespace log
}  // namespace geode
}  // namespace apache

extern "C" {

static int selector(const dirent* d) {
  std::string inputname(d->d_name);
  std::string filebasename =
      ACE::basename(apache::geode::log::globals::g_logFileWithExt->c_str());
  size_t actualHyphenPos = filebasename.find_last_of('.');
  if (strcmp(filebasename.c_str(), d->d_name) == 0) return 1;
  size_t fileExtPos = inputname.find_last_of('.');
  std::string extName = inputname.substr(fileExtPos + 1, inputname.length());
  if (strcmp(extName.c_str(), "log") != 0) return 0;
  if (fileExtPos != std::string::npos) {
    std::string tempname = inputname.substr(0, fileExtPos);
    size_t fileHyphenPos = tempname.find_last_of('-');
    if (fileHyphenPos != std::string::npos) {
      std::string buff1 = tempname.substr(0, fileHyphenPos);
      if (strstr(filebasename.c_str(), buff1.c_str()) == nullptr) {
        return 0;
      }
      if (fileHyphenPos != actualHyphenPos) return 0;
      std::string buff = tempname.substr(fileHyphenPos + 1,
                                         tempname.length() - fileHyphenPos - 1);
      for (std::string::iterator iter = buff.begin(); iter != buff.end();
           ++iter) {
        if (*iter < '0' || *iter > '9') {
          return 0;
        }
      }
      return 1;
    } else {
      return 0;
    }
  } else {
    return 0;
  }
}

static int comparator(const dirent** d1, const dirent** d2) {
  if (strlen((*d1)->d_name) < strlen((*d2)->d_name)) {
    return -1;
  } else if (strlen((*d1)->d_name) > strlen((*d2)->d_name)) {
    return 1;
  }

  int diff = std::strcmp((*d1)->d_name, (*d2)->d_name);
  if (diff < 0) {
    return -1;
  } else if (diff > 0) {
    return 1;
  } else {
    return 0;
  }
}
}

namespace apache {
namespace geode {
namespace client {

LogLevel Log::s_logLevel = LogLevel::Default;

using apache::geode::log::globals::g_bytesWritten;
using apache::geode::log::globals::g_diskSpaceLimit;
using apache::geode::log::globals::g_fileInfo;
using apache::geode::log::globals::g_fileInfoPair;
using apache::geode::log::globals::g_fileSizeLimit;
using apache::geode::log::globals::g_isLogFileOpened;
using apache::geode::log::globals::g_log;
using apache::geode::log::globals::g_logFile;
using apache::geode::log::globals::g_logFileWithExt;
using apache::geode::log::globals::g_logMutex;
using apache::geode::log::globals::g_pid;
using apache::geode::log::globals::g_rollIndex;
using apache::geode::log::globals::g_spaceUsed;
using apache::geode::log::globals::g_uname;

/*****************************************************************************/

void Log::init(LogLevel level, const char* logFileName, int32_t logFileLimit,
               int64_t logDiskSpaceLimit) {
  if (g_log != nullptr) {
    throw IllegalStateException(
        "The Log has already been initialized. "
        "Call Log::close() before calling Log::init again.");
  }
  s_logLevel = level;

  if (logDiskSpaceLimit <
      0 /*|| logDiskSpaceLimit > GEODE_MAX_LOG_DISK_LIMIT*/) {
    logDiskSpaceLimit = GEODE_MAX_LOG_DISK_LIMIT;
  }

  if (logFileLimit < 0 || logFileLimit > GEODE_MAX_LOG_FILE_LIMIT) {
    logFileLimit = GEODE_MAX_LOG_FILE_LIMIT;
  }

  std::lock_guard<decltype(g_logMutex)> guard(g_logMutex);

  if (logFileName && logFileName[0]) {
    std::string filename = logFileName;
    if (g_logFile) {
      *g_logFile = filename;
    } else {
      g_logFile = new std::string(filename);
    }

#ifdef _WIN32
    // replace all '\' with '/' to make everything easier..
    std::replace(g_logFile->begin(), g_logFile->end(), '\\', '/');
#endif

    // Appending a ".log" at the end if it does not exist or file has some other
    // extension.
    std::string filebasename = ACE::basename(g_logFile->c_str());
    int32_t len = static_cast<int32_t>(filebasename.length());
    size_t fileExtPos = filebasename.find_last_of('.', len);
    // if no extension then add .log extension
    if (fileExtPos == std::string::npos) {
      g_logFileWithExt = new std::string(*g_logFile + ".log");
    } else {
      std::string extName = filebasename.substr(fileExtPos + 1);
      // if extension other than .log change it to ext + .log
      if (extName != "log") {
        g_logFileWithExt = new std::string(*g_logFile + ".log");
      }
      // .log Extension already provided, no need to append any extension.
      else {
        g_logFileWithExt = new std::string(*g_logFile);
      }
    }

    g_fileSizeLimit = logFileLimit * 1024 * 1024;
    g_diskSpaceLimit = logDiskSpaceLimit * 1024ll * 1024ll;

    // If FileSizelimit is greater than DiskSpaceLimit & diskspaceLimit is set,
    // then set DiskSpaceLimit to FileSizelimit
    if (g_fileSizeLimit > g_diskSpaceLimit && g_diskSpaceLimit != 0) {
      g_fileSizeLimit = g_diskSpaceLimit;
    }

    // If only DiskSpaceLimit is specified and no FileSizeLimit specified, then
    // set DiskSpaceLimit to FileSizelimit.
    // This helps in getting the file handle that is exceeded the limit.
    if (g_fileSizeLimit == 0 && g_diskSpaceLimit != 0) {
      g_fileSizeLimit = g_diskSpaceLimit;
    }

    g_bytesWritten = 0;
    g_spaceUsed = 0;
    g_rollIndex = 0;

    std::string dirname = ACE::dirname(g_logFile->c_str());

    ACE_Dirent_Selector sds;
    int status = sds.open(dirname.c_str(), selector, comparator);
    if (status != -1) {
      for (int index = 0; index < sds.length(); ++index) {
        std::string strname = ACE::basename(sds[index]->d_name);
        size_t fileExtPos = strname.find_last_of('.', strname.length());
        if (fileExtPos != std::string::npos) {
          std::string tempname = strname.substr(0, fileExtPos);
          size_t fileHyphenPos = tempname.find_last_of('-', tempname.length());
          if (fileHyphenPos != std::string::npos) {
            std::string buff =
                tempname.substr(fileHyphenPos + 1, tempname.length());
            g_rollIndex = std::stoi(buff) + 1;
          }
        }  // if loop
      }    // for loop
    }
    sds.close();

    FILE* existingFile = fopen(g_logFileWithExt->c_str(), "r");
    if (existingFile != nullptr && logFileLimit > 0) {
      char rollFile[1024] = {0};
      std::string logsdirname;
      std::string logsbasename;
      std::string fnameBeforeExt;
      std::string extName;
      std::string newfilestr;

      int32_t len = static_cast<int32_t>(g_logFileWithExt->length());
      int32_t lastPosOfSep = static_cast<int32_t>(
          g_logFileWithExt->find_last_of(ACE_DIRECTORY_SEPARATOR_CHAR, len));
      if (lastPosOfSep == -1) {
        logsdirname = ".";
      } else {
        logsdirname = g_logFileWithExt->substr(0, lastPosOfSep);
      }
      logsbasename = g_logFileWithExt->substr(lastPosOfSep + 1, len);
      char logFileExtAfter = '.';
      int32_t baselen = static_cast<int32_t>(logsbasename.length());
      int32_t posOfExt = static_cast<int32_t>(
          logsbasename.find_last_of(logFileExtAfter, baselen));
      if (posOfExt == -1) {
        // throw IllegalArgument;
      } else {
        fnameBeforeExt = logsbasename.substr(0, posOfExt);
        extName = logsbasename.substr(posOfExt + 1, baselen);
      }
      std::snprintf(rollFile, 1024, "%s%c%s-%d.%s", logsdirname.c_str(),
                    ACE_DIRECTORY_SEPARATOR_CHAR, fnameBeforeExt.c_str(),
                    g_rollIndex++, extName.c_str());
      bool rollFileNameGot = false;
      while (!rollFileNameGot) {
        FILE* checkFile = fopen(rollFile, "r");
        if (checkFile != nullptr) {
          fclose(checkFile);
          checkFile = nullptr;
          std::snprintf(rollFile, 1024, "%s%c%s-%d.%s", logsdirname.c_str(),
                        ACE_DIRECTORY_SEPARATOR_CHAR, fnameBeforeExt.c_str(),
                        g_rollIndex++, extName.c_str());
        } else {
          rollFileNameGot = true;
        }
        /* adongre
         * CID 28999: Use after free (USE_AFTER_FREE)
         */
        if (checkFile != nullptr) fclose(existingFile);
      }
      // retry some number of times before giving up when file is busy etc.
      int renameResult = -1;
      int maxTries = 10;
      while (maxTries-- > 0) {
        renameResult = ACE_OS::rename(g_logFileWithExt->c_str(), rollFile);
        if (renameResult >= 0) {
          break;
        }
        // continue after some sleep
        std::this_thread::sleep_for(std::chrono::milliseconds(200));
      }
      /* (don't throw exception; try appending to existing file instead)
      if (renameResult < 0) {
        std::string msg = "Could not rename: " +
          *g_logFileWithExt + " to: " + rollFile;
        throw GeodeIOException(msg.c_str());
      }
      */
    }
    if (existingFile != nullptr) {
      fclose(existingFile);
      existingFile = nullptr;
    }
  } else if (g_logFile) {
    delete g_logFile;
    g_logFile = nullptr;
    g_logFileWithExt = nullptr;
  }
  writeBanner();
}

void Log::close() {
  std::lock_guard<decltype(g_logMutex)> guard(g_logMutex);

  std::string oldfile;

  if (g_logFile) {
    oldfile = *g_logFile;
    delete g_logFile;
    g_logFile = nullptr;
  }
  if (g_logFileWithExt) {
    delete g_logFileWithExt;
    g_logFileWithExt = nullptr;
  }

  if (g_log) {
    fclose(g_log);
    g_log = nullptr;
  }
}

void Log::writeBanner() {
  if (g_logFileWithExt == nullptr) {
    return;
  }
  const char* dirname = ACE::dirname(g_logFileWithExt->c_str());
  if (GF_FILEEXISTS(dirname) != 0 && ACE_OS::mkdir(dirname) != 0) {
    std::string msg =
        "Error in creating directories for: " + std::string(dirname);
    throw GeodeIOException(msg.c_str());
  }
  // retry some number of times before giving up when file is busy etc.
  int maxTries = 10;
  while (maxTries-- > 0) {
    g_log = fopen(g_logFileWithExt->c_str(), "a");
    if (g_log != nullptr) {
      break;
    }
    int lastError = ACE_OS::last_error();
    if (lastError != EACCES && lastError != EINTR && lastError != EWOULDBLOCK) {
      break;
    }
    // continue after some sleep
    std::this_thread::sleep_for(std::chrono::milliseconds(200));
  }
  if (!g_log) {
    g_isLogFileOpened = false;
    return;
  } else {
    g_isLogFileOpened = true;
  }

  if (s_logLevel == LogLevel::None) {
    return;
  }
  std::string bannertext = geodeBanner::getBanner();

  if (g_logFile == nullptr) {
    fprintf(stdout, "%s", bannertext.c_str());
    fflush(stdout);
    return;
  }  // else

  if (fprintf(g_log, "%s", bannertext.c_str()) == 0 || ferror(g_log)) {
    // we should be continue,
    return;
  }

  int numchars = 0;
  const char* pch = nullptr;
  pch = strchr(bannertext.c_str(), '\n');
  while (pch != nullptr) {
    pch = strchr(pch + 1, '\n');
    numchars += 2;
  }

  g_bytesWritten += static_cast<int32_t>(bannertext.length() + numchars);
  fflush(g_log);
}

const char* Log::levelToChars(LogLevel level) {
  switch (level) {
    case LogLevel::None:
      return "none";

    case LogLevel::Error:
      return "error";

    case LogLevel::Warning:
      return "warning";

    case LogLevel::Info:
      return "info";

    case LogLevel::Default:
      return "default";

    case LogLevel::Config:
      return "config";

    case LogLevel::Fine:
      return "fine";

    case LogLevel::Finer:
      return "finer";

    case LogLevel::Finest:
      return "finest";

    case LogLevel::Debug:
      return "debug";

    case LogLevel::All:
      return "all";

    default: {
      char buf[64] = {0};
      std::snprintf(buf, 64, "Unexpected log level: %d",
                    static_cast<int>(level));
      throw IllegalArgumentException(buf);
    }
  }
}

LogLevel Log::charsToLevel(const std::string& chars) {
  std::string level = chars;

  if (level.empty()) return LogLevel::None;

  std::transform(level.begin(), level.end(), level.begin(), ::tolower);

  if (level == "none") {
    return LogLevel::None;
  } else if (level == "error") {
    return LogLevel::Error;
  } else if (level == "warning") {
    return LogLevel::Warning;
  } else if (level == "info") {
    return LogLevel::Info;
  } else if (level == "default") {
    return LogLevel::Default;
  } else if (level == "config") {
    return LogLevel::Config;
  } else if (level == "fine") {
    return LogLevel::Fine;
  } else if (level == "finer") {
    return LogLevel::Finer;
  } else if (level == "finest") {
    return LogLevel::Finest;
  } else if (level == "debug") {
    return LogLevel::Debug;
  } else if (level == "all") {
    return LogLevel::All;
  } else {
    throw IllegalArgumentException(("Unexpected log level: " + level).c_str());
  }
}

char* Log::formatLogLine(char* buf, LogLevel level) {
  if (g_pid == 0) {
    g_pid = boost::this_process::get_id();
    ACE_OS::uname(&g_uname);
  }
  const size_t MINBUFSIZE = 128;
  auto now = std::chrono::system_clock::now();
  auto secs = std::chrono::system_clock::to_time_t(now);
  auto microseconds = std::chrono::duration_cast<std::chrono::microseconds>(
      now - std::chrono::system_clock::from_time_t(secs));
  auto tm_val = apache::geode::util::chrono::localtime(secs);
  auto pbuf = buf;
  pbuf += std::snprintf(pbuf, 15, "[%s ", Log::levelToChars(level));
  pbuf += std::strftime(pbuf, MINBUFSIZE, "%Y/%m/%d %H:%M:%S", &tm_val);
  pbuf += std::snprintf(pbuf, 15, ".%06" PRId64 " ",
                        static_cast<int64_t>(microseconds.count()));
  pbuf += std::strftime(pbuf, MINBUFSIZE, "%Z ", &tm_val);

  std::snprintf(pbuf, 300, "%s:%d %" PRIu64 "] ", g_uname.nodename, g_pid,
                hacks::aceThreadId(ACE_OS::thr_self()));

  return buf;
}

void Log::put(LogLevel level, const std::string& msg) {
  put(level, msg.c_str());
}

// int g_count = 0;
void Log::put(LogLevel level, const char* msg) {
  std::lock_guard<decltype(g_logMutex)> guard(g_logMutex);

  g_fileInfo fileInfo;

  char buf[256] = {0};
  char fullpath[512] = {0};

  if (!g_logFile) {
    fprintf(stdout, "%s%s\n", formatLogLine(buf, level), msg);
    fflush(stdout);
    // TODO: ignoring for now; probably store the log-lines for possible
    // future logging if log-file gets initialized properly

  } else {
    if (!g_isLogFileOpened) {
      g_log = fopen(g_logFileWithExt->c_str(), "a");
      if (!g_log) {
        g_isLogFileOpened = false;
        return;
      }
      g_isLogFileOpened = true;
    } else if (!g_log) {
      g_log = fopen(g_logFileWithExt->c_str(), "a");
      if (!g_log) {
        return;
      }
    }

    formatLogLine(buf, level);
    size_t numChars = static_cast<int>(std::strlen(buf) + std::strlen(msg));
    g_bytesWritten +=
        numChars + 2;  // bcoz we have to count trailing new line (\n)

    if ((g_fileSizeLimit != 0) && (g_bytesWritten >= g_fileSizeLimit)) {
      char rollFile[1024] = {0};
      std::string logsdirname;
      std::string logsbasename;
      std::string fnameBeforeExt;
      std::string extName;
      std::string newfilestr;

      int32_t len = static_cast<int32_t>(g_logFileWithExt->length());
      int32_t lastPosOfSep = static_cast<int32_t>(
          g_logFileWithExt->find_last_of(ACE_DIRECTORY_SEPARATOR_CHAR, len));
      if (lastPosOfSep == -1) {
        logsdirname = ".";
      } else {
        logsdirname = g_logFileWithExt->substr(0, lastPosOfSep);
      }
      logsbasename = g_logFileWithExt->substr(lastPosOfSep + 1, len);
      char logFileExtAfter = '.';
      int32_t baselen = static_cast<int32_t>(logsbasename.length());
      int32_t posOfExt = static_cast<int32_t>(
          logsbasename.find_last_of(logFileExtAfter, baselen));
      if (posOfExt == -1) {
        // throw IllegalArgument;
      } else {
        fnameBeforeExt = logsbasename.substr(0, posOfExt);
        extName = logsbasename.substr(posOfExt + 1, baselen);
      }
      std::snprintf(rollFile, 1024, "%s%c%s-%d.%s", logsdirname.c_str(),
                    ACE_DIRECTORY_SEPARATOR_CHAR, fnameBeforeExt.c_str(),
                    g_rollIndex++, extName.c_str());
      bool rollFileNameGot = false;
      while (!rollFileNameGot) {
        FILE* fp1 = fopen(rollFile, "r");
        if (fp1 != nullptr) {
          fclose(fp1);
          std::snprintf(rollFile, 1024, "%s%c%s-%d.%s", logsdirname.c_str(),
                        ACE_DIRECTORY_SEPARATOR_CHAR, fnameBeforeExt.c_str(),
                        g_rollIndex++, extName.c_str());
        } else {
          rollFileNameGot = true;
        }
      }

      fclose(g_log);
      g_log = nullptr;

      if (ACE_OS::rename(g_logFileWithExt->c_str(), rollFile) < 0) {
        return;  // no need to throw exception try next time
      }

      g_bytesWritten =
          numChars + 2;  // bcoz we have to count trailing new line (\n)
      writeBanner();
    }

    g_spaceUsed += g_bytesWritten;

    if ((g_diskSpaceLimit > 0) && (g_spaceUsed >= g_diskSpaceLimit)) {
      std::string dirname = ACE::dirname(g_logFile->c_str());
      g_spaceUsed = 0;
      ACE_stat statBuf = {};

      ACE_Dirent_Selector sds;
      int status = sds.open(dirname.c_str(), selector, comparator);
      if (status != -1) {
        for (int index = 1; index < sds.length(); ++index) {
          std::snprintf(fullpath, 512, "%s%c%s", dirname.c_str(),
                        ACE_DIRECTORY_SEPARATOR_CHAR, sds[index]->d_name);
          ACE_OS::stat(fullpath, &statBuf);
          g_fileInfoPair = std::make_pair(fullpath, statBuf.st_size);
          fileInfo.push_back(g_fileInfoPair);
          g_spaceUsed += fileInfo[index - 1].second;
        }  // for loop
        g_spaceUsed += g_bytesWritten;
        sds.close();
      }
      int fileIndex = 0;

      while ((g_spaceUsed > (g_diskSpaceLimit /*- g_fileSizeLimit*/))) {
        int64_t fileSize = fileInfo[fileIndex].second;
        if (ACE_OS::unlink(fileInfo[fileIndex].first.c_str()) == 0) {
          g_spaceUsed -= fileSize;
        } else {
          char printmsg[256];
          std::snprintf(printmsg, 256, "%s\t%s\n", "Could not delete",
                        fileInfo[fileIndex].first.c_str());
          int numChars =
              fprintf(g_log, "%s%s\n", formatLogLine(buf, level), printmsg);
          g_bytesWritten +=
              numChars + 2;  // bcoz we have to count trailing new line (\n)
        }
        fileIndex++;
      }
    }

    if ((numChars = fprintf(g_log, "%s%s\n", buf, msg)) == 0 || ferror(g_log)) {
      if ((g_diskSpaceLimit > 0)) {
        g_spaceUsed = g_spaceUsed - (numChars + 2);
      }
      if (g_fileSizeLimit > 0) {
        g_bytesWritten = g_bytesWritten - (numChars + 2);
      }

      // lets continue wothout throwing the exception; it should not cause
      // process to terminate
      fclose(g_log);
      g_log = nullptr;
    } else {
      fflush(g_log);
    }
  }
}

void Log::putThrow(LogLevel level, const char* msg, const Exception& ex) {
  std::string message = "Geode exception " + ex.getName() +
                        " thrown: " + ex.getMessage() + "\n" + msg;
  put(level, message);
}

void Log::putCatch(LogLevel level, const char* msg, const Exception& ex) {
  std::string message = "Geode exception " + ex.getName() +
                        " caught: " + ex.getMessage() + "\n" + msg;
  put(level, message);
}

void Log::enterFn(LogLevel level, const char* functionName) {
  enum { MAX_NAME_LENGTH = 1024 };
  std::string fn = functionName;
  if (fn.size() > MAX_NAME_LENGTH) {
    fn = fn.substr(fn.size() - MAX_NAME_LENGTH, MAX_NAME_LENGTH);
  }
  char buf[MAX_NAME_LENGTH + 512] = {0};
  std::snprintf(buf, 1536, "{{{===>>> Entering function %s", fn.c_str());
  put(level, buf);
}

void Log::exitFn(LogLevel level, const char* functionName) {
  enum { MAX_NAME_LENGTH = 1024 };
  std::string fn = functionName;
  if (fn.size() > MAX_NAME_LENGTH) {
    fn = fn.substr(fn.size() - MAX_NAME_LENGTH, MAX_NAME_LENGTH);
  }
  char buf[MAX_NAME_LENGTH + 512] = {0};
  std::snprintf(buf, 1536, "<<<===}}} Exiting function %s", fn.c_str());
  put(level, buf);
}

// var arg logging routines.

#ifdef _WIN32
#define vsnprintf _vsnprintf
#endif

void LogVarargs::debug(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Debug, msg);
  va_end(argp);
}

void LogVarargs::error(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Error, msg);
  va_end(argp);
}

void LogVarargs::warn(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Warning, msg);
  va_end(argp);
}

void LogVarargs::info(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Info, msg);
  va_end(argp);
}

void LogVarargs::config(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Config, msg);
  va_end(argp);
}

void LogVarargs::fine(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Fine, msg);
  va_end(argp);
}

void LogVarargs::finer(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Finer, msg);
  va_end(argp);
}

void LogVarargs::finest(const char* fmt, ...) {
  char msg[_GF_MSG_LIMIT] = {0};
  va_list argp;
  va_start(argp, fmt);
  vsnprintf(msg, _GF_MSG_LIMIT, fmt, argp);
  /* win doesn't guarantee termination */ msg[_GF_MSG_LIMIT - 1] = '\0';
  Log::put(LogLevel::Finest, msg);
  va_end(argp);
}

}  // namespace client
}  // namespace geode
}  // namespace apache

max_stars_repo_name: mreddington/geode-native

max_issues_repo_name: mreddington/geode-native

max_forks_repo_name: mreddington/geode-native


text:
#ifdef _WIN32
#include <windows.h>
#include <io.h>
#endif
#include <iostream>
#include <iomanip>
#include <string>
#include <numeric>
#include <map>
#include <vector>
#include <algorithm>
#include <array>
#include <regex>
#include <cctype>
#include <fstream>
#include <filesystem>
#include <boost/program_options.hpp>
#include "assets.hpp"
#include "string.hpp"
using namespace std;
using namespace std::filesystem;
using namespace boost::program_options;

map<char, string> res_names =
{
	// Charged (side chains often make salt bridges},
	{ 'R', "ARG" }, // Arginine,
	{ 'K', "LYS" }, // Lysine,
	{ 'D', "ASP" }, // AsparticAcid,
	{ 'E', "GLU" }, // GlutamicAcid,

	// Polar (usually participate in hydrogen bonds as proton donors or acceptors},
	{ 'Q', "GLN" }, // Glutamine,
	{ 'N', "ASN" }, // Asparagine,
	{ 'H', "HIS" }, // Histidine,
	{ 'S', "SER" }, // Serine,
	{ 'T', "THR" }, // Threonine,
	{ 'Y', "TYR" }, // Tyrosine,
	{ 'C', "CYS" }, // Cysteine,
	{ 'W', "TRP" }, // Tryptophan,

	// Hydrophobic (normally buried inside the protein core},
	{ 'A', "ALA" }, // Alanine,
	{ 'I', "ILE" }, // Isoleucine,
	{ 'L', "LEU" }, // Leucine,
	{ 'M', "MET" }, // Methionine,
	{ 'F', "PHE" }, // Phenylalanine,
	{ 'V', "VAL" }, // Valine,
	{ 'P', "PRO" }, // Proline,
	{ 'G', "GLY" }, // Glycine
};

enum class headers
{
	symbol,
	gene,
	uniprot,
	residue,
	sequence,
	numbering,
};

array<pair<int, string>, 6> header_fmts =
{ {
	{ 14, "Protein" },
	{ 9,  "Gene" },
	{ 10, "Uniprot" },
	{ 5,  "Res" },
	{ 6,  "Seq" },
	{ 0,  "Numbering" },
} };

// see https://en.wikipedia.org/wiki/ANSI_escape_code#Colors
enum class fgcolor
{
	none    = 0,
	black   = 30, // Black   30 40
	red     = 31, // Red     31 41
	green   = 32, // Green   32 42
	yellow  = 33, // Yellow  33 43
	blue    = 34, // Blue    34 44
	magenta = 35, // Magenta 35 45
	cyan    = 36, // Cyan    36 46
	white   = 37, // White   37 47
	bright_black   = 90, // Bright Black   90 100
	bright_red     = 91, // Bright Red     91 101
	bright_green   = 92, // Bright Green   92 102
	bright_yellow  = 93, // Bright Yellow  93 103
	bright_blue    = 94, // Bright Blue    94 104
	bright_magenta = 95, // Bright Magenta 95 105
	bright_cyan    = 96, // Bright Cyan    96 106
	bright_white   = 97, // Bright White   97 107
};

enum class bgcolor
{
	none    = 0,
	black   = 40, // Black   30 40
	red     = 41, // Red     31 41
	green   = 42, // Green   32 42
	yellow  = 43, // Yellow  33 43
	blue    = 44, // Blue    34 44
	magenta = 45, // Magenta 35 45
	cyan    = 46, // Cyan    36 46
	white   = 47, // White   37 47
	bright_black   = 100, // Bright Black   90 100
	bright_red     = 101, // Bright Red     91 101
	bright_green   = 102, // Bright Green   92 102
	bright_yellow  = 103, // Bright Yellow  93 103
	bright_blue    = 104, // Bright Blue    94 104
	bright_magenta = 105, // Bright Magenta 95 105
	bright_cyan    = 106, // Bright Cyan    96 106
	bright_white   = 107, // Bright White   97 107
};

set<string> colorings
{
	"always",
	"auto",
	"never",
};

set<string> listings
{
	"schemes",
	"residues",
	"symbols",
	"symbol_species",
	"genes",
	"pdbids",
	"uniprots",
};

#ifdef _WIN32

bool is_redirected(FILE* file)
{
	return !_isatty(_fileno(file));
}

// see https://docs.microsoft.com/en-us/windows/console/console-virtual-terminal-sequences#example
void init_console_coloring()
{
	HANDLE hOut = GetStdHandle(STD_OUTPUT_HANDLE);
	if (hOut == INVALID_HANDLE_VALUE)
		return;

	DWORD dwMode = 0;
	if (!GetConsoleMode(hOut, &dwMode))
		return;

	dwMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING;
	if (!SetConsoleMode(hOut, dwMode))
		return;
}

#else // __APPLE__ || __linux__ || __unix__ || defined(_POSIX_VERSION)

bool is_redirected(FILE* file)
{
	return !isatty(fileno(file));
}

void init_console_coloring()
{
}

#endif

template <class _Traits>
inline basic_ostream<char, _Traits>& operator<<(basic_ostream<char, _Traits>& _Ostr,
	const fgcolor& color)
{
	return _Ostr << "\x1b[" << (int)color << "m";
}

bool iequals(const string& a, const string& b)
{
	for (size_t i = 0; i < a.size() || i < b.size(); ++i)
	{
		if (i >= a.size())
		{
			if (!isspace(b[i])) return false;
		}
		else if (i >= b.size())
		{
			if (!isspace(a[i])) return false;
		}
		else if (tolower(a[i]) != tolower(b[i]))
		{
			return false;
		}
	}
	return true;
}

int match_scheme(const string& s)
{
	for (int i = 0; i < (int)schemes.size(); i++)
		for (auto& name : get<2>(schemes[i]))
			if (iequals(s, name))
				return i;
	return -1;
}

void supported_schemes(const string& default_scheme)
{
	cout << "Supported schemes:" << endl;

	for (auto [offset, width, abbrs] : schemes)
	{
		bool first = true;
		string s;
		for (auto it = abbrs.rbegin(); it != abbrs.rend() - 1; ++it)
		{
			if (!first)
				s += ", ";
			s += *it;
			first = false;
		}
		cout << "  " << left << setw(16) << s;
		cout << abbrs.front();
		cout << (find(abbrs.begin(), abbrs.end(), default_scheme) != abbrs.end() ? " -> DEFAULT" : "") << endl;
	}
}

bool get_index_for_seq(const string& uniprot, int seq, int& index, char& res_name)
{
	auto [min_seq, res_count, res_names, numbering] = numbering_data[uniprot];
	if (seq < min_seq || seq >= min_seq + res_count || numbering[seq - min_seq] == -1)
		return false;
	index = numbering[seq - min_seq];
	res_name = res_names[seq - min_seq];
	return true;
}

void output_line(const array<bool, header_fmts.size()>& no_cols, int last_col, const string& scheme)
{
	for (int i = 0; i < (int)header_fmts.size(); i++)
	{
		if (no_cols[i])
			continue;
		if (i != last_col)
			cout << left << setw(header_fmts[i].first);
		cout << header_fmts[i].second;
		if (i == last_col)
			cout << endl;
	}
}

void output_line(const array<bool, header_fmts.size()>& no_cols, int last_col, const array<bool, header_fmts.size()>& highlights, const string& uniprot, const string& seq, const string& numbering, const char& res_name, fgcolor hlcolor)
{
	auto [symbol, species, gene_name, long_species] = uniprot_dict[uniprot];

	vector<string> fields
	{
		symbol + '_' + species,
		gene_name,
		uniprot,
		res_names.count(res_name) ? res_names[res_name] : "?",
		res_names.count(res_name) ? res_name + seq : "?" + seq,
		numbering,
	};

	for (int i = 0; i < (int)header_fmts.size(); i++)
	{
		if (no_cols[i])
			continue;
		if (highlights[i] && hlcolor != fgcolor::none)
			cout << hlcolor;
		if (i != last_col)
			cout << left << setw(header_fmts[i].first);
		cout << fields[i];
		if (highlights[i] && hlcolor != fgcolor::none)
			cout << fgcolor::none;
		if (i == last_col)
			cout << endl;
	}
}

int process(const array<bool, header_fmts.size()>& no_cols, int last_col, bool no_headers, bool show_unmatched, int scheme_id, int& line_no, const string& query, fgcolor hlcolor)
{
	smatch ms;
	if (!regex_match(query, ms, regex("([^:]*):(.*)")))
	{
		cerr << "ERROR: invalid query '" << query << "'; the correct form is '<target>:<numbering>'" << endl;
		return 2;
	}

	string target = ms[1].str(), numbering = ms[2].str();

	if (target.empty() && numbering.empty())
	{
		cerr << "ERROR: invalid query '" << query << "'; at least a target or a numbering is required" << endl;
		return 2;
	}

	vector<string> uids;
	transform(target.begin(), target.end(), target.begin(), ::toupper);
	transform(numbering.begin(), numbering.end(), numbering.begin(), ::tolower);

	array<bool, header_fmts.size()> highlights{};

	// only target is blank
	if (target.empty())
	{
		for (auto [uid, pn] : uniprot_dict)
			uids.push_back(uid);
	}
	// uniprot_id: P28223
	// species: Human
	else if (uniprot_dict.count(target))
	{
		highlights[(int)headers::uniprot] = true;
		uids.push_back(target);
	}
	// pdb_id: 6A93
	else if (pdb_id_dict.count(target)) // unique
	{
		//highlights[(int)headers::pdbid] = true;
		uids.push_back(pdb_id_dict[target]);
	}
	// gene name: HTR2A
	else if (gene_name_dict.count(target)) // could be multiple
	{
		highlights[(int)headers::gene] = true;
		auto [lo, hi] = gene_name_dict.equal_range(target);
		for (; lo != hi; ++lo)
			uids.push_back(lo->second);
	}
	// protein_symbol_species: 5HT2A_HUMAN
	else if (symbol_species_dict.count(target)) // unique
	{
		highlights[(int)headers::symbol] = true;
		uids.push_back(symbol_species_dict[target]);
	}
	// protein_symbol: 5HT2A
	else if (symbol_dict.count(target)) // could be multiple
	{
		highlights[(int)headers::symbol] = true;
		auto [lo, hi] = symbol_dict.equal_range(target);
		for (; lo != hi; ++lo)
			uids.push_back(lo->second);
	}
	else
	{
		cerr << "ERROR: unknown target '" << ms[1].str() << "'; use uniprot id, gene name, protein symbol or pdb id for a GPCR" << endl;
		return 2;
	}

	auto [offset, width, names] = schemes[scheme_id];

	// all residue numberings
	if (numbering.empty())
	{
		if (!no_headers && !line_no)
		{
			output_line(no_cols, last_col, names[1]);
			++line_no;
		}
		for (auto& uid : uids)
		{
			auto [min_seq, seq_count, seq_names, numbering] = numbering_data[uid];
			for (int seq = min_seq; seq < min_seq + seq_count; seq++)
			{
				int stridx;
				char res_name;
				if (get_index_for_seq(uid, seq, stridx, res_name))
				{
					output_line(no_cols, last_col, highlights, uid, to_string(seq), string_table[stridx].substr(offset, width), res_name, hlcolor);
					++line_no;
				}
			}
		}
	}
	// numbering is a residue sequence
	else if (count_if(numbering.begin(), numbering.end(), ::isdigit) == (int)numbering.size())
	{
		highlights[(int)headers::sequence] = true;
		if (!no_headers && !line_no)
		{
			output_line(no_cols, last_col, names[1]);
			++line_no;
		}
		int seq = stoi(numbering);
		for (auto& uid : uids)
		{
			int stridx;
			char res_name;
			if (get_index_for_seq(uid, seq, stridx, res_name))
			{
				output_line(no_cols, last_col, highlights, uid, to_string(seq), string_table[stridx].substr(offset, width), res_name, hlcolor);
				++line_no;
			}
			else if (show_unmatched)
			{
				output_line(no_cols, last_col, highlights, uid, to_string(seq), "?", '?', hlcolor);
				++line_no;
			}
		}
	}
	// numbering is a residue numbering
	else if (numbering.size() <= width)
	{
		highlights[(int)headers::numbering] = true;
		if (!no_headers && !line_no)
		{
			output_line(no_cols, last_col, names[1]);
			++line_no;
		}
		for (auto& uid : uids)
		{
			auto [min_seq, seq_count, seq_names, numbering2] = numbering_data[uid];
			bool hit = false;

			for (int seq = min_seq; seq < min_seq + seq_count; seq++)
			{
				int stridx;
				char res_name;
				if (!get_index_for_seq(uid, seq, stridx, res_name))
					continue;

				auto str = string_table[stridx].substr(offset, width);
				hit = iequals(str, numbering);

				if (hit)
				{
					output_line(no_cols, last_col, highlights, uid, to_string(seq), str, res_name, hlcolor);
					++line_no;
					break;
				}
			}

			if (!hit && show_unmatched)
			{
				output_line(no_cols, last_col, highlights, uid, "?", ms[2].str(), '?', hlcolor);
				++line_no;
			}
		}
	}
	// unknown numbering
	else
	{
		cerr << "ERROR: invalid numbering '" << ms[2].str() << "' for scheme '" << names[0] << "'" << endl;
		return 2;
	}

	return 0;
}

string formatter(const set<string>& set)
{
	string r;
	string last;
	for (auto& s : set)
	{
		if (!last.empty())
		{
			r.push_back('\'');
			r += last;
			r += "', ";
		}
		last = s;
	}
	if (!last.empty())
	{
		r += "or '";
		r += last;
		r.push_back('\'');
	}
	return r;
}

int main(int argc, char* argv[])
{
	static string default_scheme = "BW", default_coloring = "auto";
	static fgcolor default_hlcolor = fgcolor::bright_red;

	try
	{
		vector<string> queries;
		path file;
		string scheme, listing, coloring;
		bool no_headers, show_unmatched, ignore_errors;
		array<bool, header_fmts.size()> no_cols{};
		fgcolor hlcolor = fgcolor::none;

		options_description input_options("Input options");
		input_options.add_options()
			("query,q", value<vector<string>>(&queries)->value_name("QUERY ..."), "a list of case-insensitive queries; QUERY must be in the format of <target>:<numbering> where <target> is any of: uniprot id, gene name, protein symbol or pdb id, <numbering> is either a residue sequence number or a residue numbering in the scheme specified by --scheme argument")
			("file,f", value<path>(&file)->value_name("FILE"), "use queries in the specified file")
			("scheme,s", value<string>(&scheme)->default_value(default_scheme)->value_name("KEYWORD"), "a case-insensitive keyword to match a GPCR numbering scheme; supported schemes are listed with --list schemes")
			;

		options_description output_options("Output options");
		output_options.add_options()
			(",1", bool_switch(&no_cols[0]), "suppress column 1 (Protein Symbol)")
			(",2", bool_switch(&no_cols[1]), "suppress column 2 (Gene Name)")
			(",3", bool_switch(&no_cols[2]), "suppress column 3 (Uniprot Id)")
			(",4", bool_switch(&no_cols[3]), "suppress column 4 (Residue Name)")
			(",5", bool_switch(&no_cols[4]), "suppress column 5 (Residue Sequence)")
			(",6", bool_switch(&no_cols[5]), "suppress column 6 (Residue Numbering)")
			("color", value<string>(&coloring)->value_name("WHEN")->default_value(default_coloring), ("colorize the output; WHEN can be " + formatter(colorings) + "; default to 'auto' if omitted").c_str())
			("hide-headers,H", bool_switch(&no_headers), "do not display headers on the first line")
			("show-unmatched,u", bool_switch(&show_unmatched), "output unmatched numberings as well (will be labeled with a question mark ?)")
			("ignore-errors,E", bool_switch(&ignore_errors), "ignore errors and move on to the next query")
			;

		options_description misc_options("Misc options");
		misc_options.add_options()
			("list,L", value<string>(&listing)->value_name("TYPE"), ("show a supported list; TYPE can be " + formatter(listings)).c_str())
			("help", "this help information")
			("version", "version information")
			;

		options_description all_options;
		all_options.add(input_options).add(output_options).add(misc_options);

		positional_options_description positional;
		positional.add("query", -1);

		variables_map vm;
		store(command_line_parser(argc, argv).options(all_options).positional(positional).run(), vm);
		notify(vm);

		if (vm.count("help")) // program input
		{
			cout << "Usage: " << argv[0] << " [--query] <query1> [<query2> <query3> ...] [options]" << endl;
			cout << "       " << argv[0] << " --file <query-file> [options]" << endl;
			cout << "GPCR numbering tool by Maozi Chen" << endl;
			cout << "All data are downloaded from https://GPCRdb.org/structure/" << endl;
			cout << all_options << endl;
			cout << "Examples:" << endl;
			cout << "  " << argv[0] << " 5HT2A:123     \tGet BW numbering for protein 5HT2A at 123." << endl;
			cout << "  " << argv[0] << " HTR2A:123     \tGet BW numbering for gene HTR2A at 123." << endl;
			cout << "  " << argv[0] << " P28223:123    \tGet BW numbering for uniprot id P28223 at 123." << endl;
			cout << "  " << argv[0] << " 6A93:123      \tGet BW numbering for pdb id 6A93 at 123." << endl;
			cout << "  " << argv[0] << " :123          \tGet BW numberings for all GPCR proteins at 123." << endl;
			cout << "  " << argv[0] << " 6A93:2.53     \tGet residue name in form Y139 for pdb 6A93 at BW 2.53." << endl;
			cout << "  " << argv[0] << " HTR2A:        \tGet all BW numberings for gene HTR2A." << endl;
			cout << "  " << argv[0] << " :2.53         \tGet residue sequence numbers for all GPCR at BW 2.53." << endl;
			cout << "  " << argv[0] << " HTR2A:123 -sWB\tGet Wootten numberings for gene HTR2A at 123." << endl;
			return 0;
		}

		if (vm.count("list"))
		{
			if (!listings.count(listing))
			{
				cerr << "ERROR: unrecognized argument '" << listing << "'; use " << formatter(listings) << endl;
				return 2;
			}

			if (listing == "schemes")
			{
				supported_schemes(default_scheme);
			}
			else if (listing == "residues")
			{
				for (auto [abbr, name] : res_names)
					cout << abbr << '\t' << name << endl;
			}
			else
			{
				set<string> results;
				if (listing == "symbol_species")
				{
					for (auto [key, ignore] : symbol_species_dict)
						results.insert(key);
				}
				else if (listing == "genes")
				{
					for (auto [key, ignore] : gene_name_dict)
						results.insert(key);
				}
				else if (listing == "symbols")
				{
					for (auto [key, ignore] : symbol_dict)
						results.insert(key);
				}
				else if (listing == "pdbids")
				{
					for (auto [key, ignore] : pdb_id_dict)
						results.insert(key);
				}
				else if (listing == "uniprots")
				{
					for (auto [key, ignore] : uniprot_dict)
						results.insert(key);
				}

				for (auto& s : results)
					cout << s << endl;
			}

			return 0;
		}

		if (vm.count("version"))
		{
			cout << "gpcrn version: 1.0.8 (2021-06-02)" << endl;
			cout << "GPCRdb version: 2021-05-14" << endl;
			return 0;
		}

		// find a scheme name match
		int scheme_id = match_scheme(scheme);
		if (scheme_id == -1)
		{
			set<string> keywords;
			for (auto [ignore, also_ignore, abbrs] : schemes)
				keywords.insert(abbrs[1]);
			cerr << "ERROR: unrecognized argument '" << scheme << "'; use " << formatter(keywords) << "; see more with '--list schemes'" << endl;
			return 2;
		}

		header_fmts.back().second = (get<2>(schemes[scheme_id]))[1];

		// apply coloring config
		if (!colorings.count(coloring))
		{
			cerr << "ERROR: unrecognized argument '" << coloring << "'; use " << formatter(colorings) << endl;
			return 2;
		}

		if (coloring == "always" || (coloring == "auto" && !is_redirected(stdout)))
		{
			hlcolor = default_hlcolor;
			init_console_coloring();
		}

		// find the last column number
		int last_col = 0;
		for (last_col = 5; last_col >= 0; --last_col)
			if (!no_cols[last_col])
				break;

		// start running
		int line_no = 0;
		bool any = false;
		if (queries.size())
		{
			for (auto& query : queries)
			{
				int retcode = process(no_cols, last_col, no_headers, show_unmatched, scheme_id, line_no, query, hlcolor);
				if (!ignore_errors && retcode)
					return retcode;
			}
			any = true;
		}

		if (vm.count("file"))
		{
			ifstream in(file);
			for (string line; safe_getline(in, line);)
			{
				trim(line);
				if (line.empty() || line[0] == '#')
					continue;
				int retcode = process(no_cols, last_col, no_headers, show_unmatched, scheme_id, line_no, line, hlcolor);
				if (!ignore_errors && retcode)
					return retcode;
			}
			any = true;
		}

		if (!any)
		{
			for (string line; safe_getline(cin, line);)
			{
				trim(line);
				if (line.empty() || line[0] == '#')
					continue;
				int retcode = process(no_cols, last_col, no_headers, show_unmatched, scheme_id, line_no, line, hlcolor);
				if (!ignore_errors && retcode)
					return retcode;
			}
		}
		return 0;
	}
	catch (exception& ex)
	{
		cerr << "ERROR: " << ex.what() << endl;
		return 2;
	}
}

ext: cpp

max_stars_repo_name: stcmz/gpcrn

max_issues_repo_name: stcmz/gpcrn

max_forks_repo_name: stcmz/gpcrn


text:
#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"

#include <queue>
#include <boost/container/flat_set.hpp>
#include <storm-pars/analysis/MonotonicityChecker.h>

#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/vector.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"

#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/NotSupportedException.h"

namespace storm {
    namespace modelchecker {

        template <typename SparseModelType, typename ConstantType>
        SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker() {
            //Intentionally left empty
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(Environment const& env, storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {

            currentFormula = checkTask.getFormula().asSharedPointer();
            currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());

            if (currentCheckTask->getFormula().isProbabilityOperatorFormula()) {
                auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula();
                if(probOpFormula.getSubformula().isBoundedUntilFormula()) {
                    specifyBoundedUntilFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
                } else if(probOpFormula.getSubformula().isUntilFormula()) {
                    specifyUntilFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
                } else if (probOpFormula.getSubformula().isEventuallyFormula()) {
                    specifyReachabilityProbabilityFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
                } else {
                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
                }
            } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) {
                auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula();
                if(rewOpFormula.getSubformula().isEventuallyFormula()) {
                    specifyReachabilityRewardFormula(env, currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
                } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) {
                    specifyCumulativeRewardFormula(env, currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
                }
            }
        }

        template <typename SparseModelType, typename ConstantType>
        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion, std::shared_ptr<storm::analysis::Order> reachabilityOrder, std::shared_ptr<storm::analysis::LocalMonotonicityResult<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType>> localMonotonicityResult) {
            typedef typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType VariableType;
            typedef typename storm::analysis::MonotonicityResult<VariableType>::Monotonicity Monotonicity;
            typedef typename storm::utility::parametric::Valuation<typename SparseModelType::ValueType> Valuation;
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
            STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
            STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
            STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");

            RegionResult result = initialResult;

            // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
            if (hypothesis == RegionResultHypothesis::Unknown && result == RegionResult::Unknown) {
                result = getInstantiationChecker().check(env, region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
            }

            bool existsSat = (hypothesis == RegionResultHypothesis::AllSat || result == RegionResult::ExistsSat || result == RegionResult::CenterSat);
            bool existsViolated = (hypothesis == RegionResultHypothesis::AllViolated || result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated);

            // Here we check on global monotonicity
            if (localMonotonicityResult != nullptr && localMonotonicityResult->isDone()) {
                // Try to check it with a global monotonicity result
                auto monRes = localMonotonicityResult->getGlobalMonotonicityResult();
                bool lowerBound = isLowerBound(this->currentCheckTask->getBound().comparisonType);

                if (monRes->isDone() && monRes->isAllMonotonicity()) {
                    // Build valuations
                    auto monMap = monRes->getMonotonicityResult();
                    Valuation valuationToCheckSat;
                    Valuation valuationToCheckViolated;
                    for (auto var : region.getVariables()) {
                        auto monVar = monMap[var];
                        if (monVar == Monotonicity::Constant) {
                            valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                            valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                        } else if (monVar == Monotonicity::Decr) {
                            if (lowerBound) {
                                valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
                                valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                            } else {
                                valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                                valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
                            }
                        } else if (monVar == Monotonicity::Incr) {
                            if (lowerBound) {
                                valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                                valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
                            } else {
                                valuationToCheckSat.insert(std::pair<VariableType, CoefficientType>(var, region.getUpperBoundary(var)));
                                valuationToCheckViolated.insert(std::pair<VariableType, CoefficientType>(var, region.getLowerBoundary(var)));
                            }
                        }
                    }

                    // Check for result
                    if (existsSat && getInstantiationCheckerSAT().check(env, valuationToCheckSat)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                        STORM_LOG_INFO("Region " << region << " is AllSat, discovered with instantiation checker on " << valuationToCheckSat << " and help of monotonicity" << std::endl);
                        RegionModelChecker<typename SparseModelType::ValueType>::numberOfRegionsKnownThroughMonotonicity++;
                        return RegionResult::AllSat;
                    }

                    if (existsViolated && !getInstantiationCheckerVIO().check(env, valuationToCheckViolated)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                        STORM_LOG_INFO("Region " << region << " is AllViolated, discovered with instantiation checker on " << valuationToCheckViolated << " and help of monotonicity" << std::endl);
                        RegionModelChecker<typename SparseModelType::ValueType>::numberOfRegionsKnownThroughMonotonicity++;
                        return RegionResult::AllViolated;
                    }

                    return RegionResult::ExistsBoth;
                }
            }

            // Try to prove AllSat or AllViolated, depending on the hypothesis or the current result
            if (existsSat) {
                // show AllSat:
                storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
                auto checkResult = this->check(env, region, parameterOptimizationDirection, reachabilityOrder, localMonotonicityResult);
                if (checkResult->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                    result = RegionResult::AllSat;
                } else if (sampleVerticesOfRegion) {
                    result = sampleVertices(env, region, result);
                }
            } else if (existsViolated) {
                // show AllViolated:
                storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
                auto checkResult = this->check(env, region, parameterOptimizationDirection, reachabilityOrder, localMonotonicityResult);
                if (!checkResult->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                    result = RegionResult::AllViolated;
                } else if (sampleVerticesOfRegion) {
                    result = sampleVertices(env, region, result);
                }
            } else {
                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
            }
            return result;
        }

        template <typename SparseModelType, typename ConstantType>
        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::sampleVertices(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
            RegionResult result = initialResult;

            if (result == RegionResult::AllSat || result == RegionResult::AllViolated) {
                return result;
            }

            bool hasSatPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
            bool hasViolatedPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;

            // Check if there is a point in the region for which the property is satisfied
            auto vertices = region.getVerticesOfRegion(region.getVariables());
            auto vertexIt = vertices.begin();
            while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
                if (getInstantiationChecker().check(env, *vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                    hasSatPoint = true;
                } else {
                    hasViolatedPoint = true;
                }
                ++vertexIt;
            }

            if (hasSatPoint) {
                if (hasViolatedPoint) {
                    result = RegionResult::ExistsBoth;
                } else if (result != RegionResult::CenterSat) {
                    result = RegionResult::ExistsSat;
                }
            } else if (hasViolatedPoint && result != RegionResult::CenterViolated) {
                result = RegionResult::ExistsViolated;
            }

            return result;
        }

        template <typename SparseModelType, typename ConstantType>
        std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters, std::shared_ptr<storm::analysis::Order> reachabilityOrder, std::shared_ptr<storm::analysis::LocalMonotonicityResult<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType>> localMonotonicityResult) {
            auto quantitativeResult = computeQuantitativeValues(env, region, dirForParameters, localMonotonicityResult);
            lastValue = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
            if(currentCheckTask->getFormula().hasQuantitativeResult()) {
                return quantitativeResult;
            } else {
                return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
            }
        }

        template <typename SparseModelType, typename ConstantType>
        std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters, std::shared_ptr<storm::analysis::LocalMonotonicityResult<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType>> localMonotonicityResult) {
            STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula...");
            return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(computeQuantitativeValues(env, region, dirForParameters, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>()));
        }

        template <typename SparseModelType, typename ConstantType>
        typename SparseModelType::ValueType SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
            STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state.");
            return storm::utility::convertNumber<typename SparseModelType::ValueType>(getBound(env, region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
        }

        template <typename SparseModelType, typename ConstantType>
        storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationCheckerSAT() {
            return getInstantiationChecker();
        }

        template <typename SparseModelType, typename ConstantType>
        storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationCheckerVIO() {
            return getInstantiationChecker();
        }

        template <typename SparseModelType, typename ConstantType>
        struct RegionBound {
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType VariableType;

            RegionBound(RegionBound<SparseModelType, ConstantType> const& other) = default;
            RegionBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& r, std::shared_ptr<storm::analysis::Order> o, std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> l, ConstantType const& b) : region(r), order(o), localMonRes(l), bound(b) {}
            storm::storage::ParameterRegion<typename SparseModelType::ValueType> region;
            std::shared_ptr<storm::analysis::Order> order;
            std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonRes;
            ConstantType bound;
        };

        template <typename SparseModelType, typename ConstantType>
        std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::computeExtremalValue(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dir, typename SparseModelType::ValueType const& precision) {
            return computeExtremalValue(env, region, dir, precision, boost::none);
        }

        // TODO: this is not efficient
        template <typename SparseModelType, typename ConstantType>
        bool SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::checkExtremalValue(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dir, typename SparseModelType::ValueType const& precision, typename SparseModelType::ValueType const& valueToCheck) {
            auto res = computeExtremalValue(env, region, dir, precision, storm::utility::convertNumber<ConstantType>(valueToCheck)).first;
            auto diff = storm::utility::convertNumber<ConstantType>(valueToCheck) - storm::utility::convertNumber<ConstantType>(res);
            return (diff >= (-storm::utility::convertNumber<ConstantType>(precision)) && diff <= storm::utility::convertNumber<ConstantType>(precision));
        }

        template <typename SparseModelType, typename ConstantType>
        SparseModelType const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
            return *parametricModel;
        }

        template <typename SparseModelType, typename ConstantType>
        CheckTask<storm::logic::Formula, ConstantType> const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentCheckTask() const {
            return *currentCheckTask;
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(Environment const& env, CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(Environment const& env, CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityProbabilityFormula(Environment const& env, CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
            // transform to until formula
            auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer());
            specifyUntilFormula(env, currentCheckTask->substituteFormula(*untilFormula));
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(Environment const& env, CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
        }

        template <typename SparseModelType, typename ConstantType>
        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(Environment const& env, CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
        }

        template<typename SparseModelType, typename ConstantType>
        std::shared_ptr<storm::analysis::Order> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::copyOrder(std::shared_ptr<storm::analysis::Order> order) {
            auto res = order->copy();
            if (orderExtender) {
                orderExtender->setUnknownStates(order, res);
                orderExtender->copyMinMax(order, res);
            }
            return res;
        }

        template<typename SparseModelType, typename ConstantType>
        std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::checkForPossibleMonotonicity(Environment const& env,
                                                                                const storage::ParameterRegion<typename SparseModelType::ValueType> &region,
                                                                                std::set<VariableType>& possibleMonotoneIncrParameters,
                                                                                std::set<VariableType>& possibleMonotoneDecrParameters,
                                                                                std::set<VariableType>& possibleNotMonotoneParameters,
                                                                                std::set<VariableType>const& consideredVariables,
                                                                                storm::solver::OptimizationDirection const& dir) {
            bool minimize = storm::solver::minimize(dir);
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation Valuation;
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
            ConstantType value = storm::solver::minimize(dir) ? 1 : 0;
            Valuation valuation;
            for (auto& var : consideredVariables) {
                ConstantType previousCenter = -1;
//                ConstantType previousUpper = -1;
//                ConstantType previousLower = -1;
                bool monDecr = true;
                bool monIncr = true;
                auto valuationCenter = region.getCenterPoint();
//                auto valuationLower = region.getLowerBoundaries();
//                auto valuationUpper = region.getUpperBoundaries();

                valuationCenter[var] = region.getLowerBoundary(var);
//                valuationLower[var] = region.getLowerBoundary(var);
//                valuationUpper[var] = region.getLowerBoundary(var);
                // TODO: make cmdline argument or 1/precision
                int numberOfSamples = 50;
                auto stepSize = (region.getUpperBoundary(var) - region.getLowerBoundary(var)) / (numberOfSamples - 1);

                while (valuationCenter[var] <= region.getUpperBoundary(var)) {
                    // Create valuation
//                    assert (valuationLower[var] <= region.getUpperBoundary(var));
//                    assert (valuationUpper[var] <= region.getUpperBoundary(var));
//
//                    ConstantType valueLower = getInstantiationChecker().check(env, valuationLower)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
                    ConstantType valueCenter = getInstantiationChecker().check(env, valuationCenter)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
//                    ConstantType valueUpper = getInstantiationChecker().check(env, valuationUpper)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
//                    if (storm::solver::minimize(dir) ? valueLower <= value : valueLower >= value) {
//                        value = valueLower;
//                        valuation = valuationLower;
//                    }
                    if (storm::solver::minimize(dir) ? valueCenter <= value : valueCenter >= value) {
                        value = valueCenter;
                        valuation = valuationCenter;
                    }
//                    if (storm::solver::minimize(dir) ? valueUpper <= value : valueUpper >= value) {
//                        value = valueUpper;
//                        valuation = valuationUpper;
//                    }
                    // Calculate difference with result for previous valuation
                    ConstantType diffCenter = previousCenter - valueCenter;
//                    ConstantType diffLower = previousLower - valueLower;
//                    ConstantType diffUpper = previousUpper - valueUpper;
                    assert (previousCenter == -1 || (diffCenter >= -1 && diffCenter <= 1));
//                    assert (previousUpper == -1 || (diffUpper >= -1 && diffUpper <= 1));
//                    assert (previousLower == -1 || (diffLower >= -1 && diffLower <= 1));
//
                    if (previousCenter != -1) {
                        assert (previousCenter != -1 && previousCenter != -1);
                        monDecr &= diffCenter > 0 && diffCenter > 0 && diffCenter > 0; // then previous value is larger than the current value from the initial states
                        monIncr &= diffCenter < 0 && diffCenter < 0 && diffCenter < 0;
//                    } else {
//                        assert (previousUpper == -1 && previousLower == -1);
                    }
                    previousCenter = valueCenter;
//                    previousLower = valueLower;
//                    previousUpper = valueUpper;
                    if (!monDecr && ! monIncr) {
                        break;
                    }
                    valuationCenter[var] += stepSize;
//                    valuationLower[var] += stepSize;
//                    valuationUpper[var] += stepSize;
                }
                if (monIncr) {
                    possibleMonotoneParameters.insert(var);
                    possibleMonotoneIncrParameters.insert(var);
                } else if (monDecr) {
                    possibleMonotoneParameters.insert(var);
                    possibleMonotoneDecrParameters.insert(var);
                } else {
                    possibleNotMonotoneParameters.insert(var);
                }
            }
            return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));

        }

        template<typename SparseModelType, typename ConstantType>
        std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::computeExtremalValue(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dir, typename SparseModelType::ValueType const& precision, boost::optional<ConstantType> const& initialValue) {
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
            STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting extremal values at the initial state requires a model with a single initial state.");
            bool const useMonotonicity = this->isUseMonotonicitySet();
            bool const minimize = storm::solver::minimize(dir);

            // Comparator for the region queue
            auto cmp = storm::solver::minimize(dir) ?
                       [](RegionBound<SparseModelType, ConstantType> const& lhs, RegionBound<SparseModelType, ConstantType> const& rhs) { return lhs.bound > rhs.bound; } :
                       [](RegionBound<SparseModelType, ConstantType> const& lhs, RegionBound<SparseModelType, ConstantType> const& rhs) { return lhs.bound < rhs.bound; };
            std::priority_queue<RegionBound<SparseModelType, ConstantType>, std::vector<RegionBound<SparseModelType, ConstantType>>, decltype(cmp)> regionQueue(cmp);
            storm::utility::Stopwatch initialWatch(true);

            storm::utility::Stopwatch boundsWatch(false);
            auto numberOfPLACallsBounds = 0;
            if (useMonotonicity) {
                if (this->isUseBoundsSet()) {
                    numberOfPLACallsBounds++;
                    numberOfPLACallsBounds++;
                    orderExtender->setMinValuesOnce(getBound(env, region, storm::solver::OptimizationDirection::Minimize, nullptr)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                    orderExtender->setMaxValuesOnce(getBound(env, region, storm::solver::OptimizationDirection::Maximize, nullptr)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                }
                auto order = this->extendOrder(env, nullptr, region);
                auto monRes = std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>>(new storm::analysis::LocalMonotonicityResult<VariableType>(order->getNumberOfStates()));
                storm::utility::Stopwatch monotonicityWatch(true);
                this->extendLocalMonotonicityResult(region, order, monRes);
                monotonicityWatch.stop();
                STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl << std::endl);

                if (minimize) {
                    regionQueue.emplace(region, order, monRes, storm::utility::zero<ConstantType>());
                } else {
                    regionQueue.emplace(region, order, monRes, storm::utility::one<ConstantType>());
                }
            } else {
                if (minimize) {
                    regionQueue.emplace(region, nullptr, nullptr, storm::utility::zero<ConstantType>());
                } else {
                    regionQueue.emplace(region, nullptr, nullptr, storm::utility::one<ConstantType>());
                }
            }

            // The results
            boost::optional<ConstantType> value;
            typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation valuation;
            if (!initialValue) {
                auto init = getGoodInitialPoint(env, region, dir, regionQueue.top().localMonRes);
                value = storm::utility::convertNumber<ConstantType>(init.first);
                valuation = std::move(init.second);
            } else {
                value = initialValue;
            }

            initialWatch.stop();
            STORM_PRINT(std::endl << "Total time for initial points: " << initialWatch << "." << std::endl << std::endl);
            if (!initialValue) {
                STORM_LOG_INFO("Initial value: " << value.get() << " at " << valuation);
            }

            auto numberOfSplits = 0;
//            auto count = 0;
            auto numberOfPLACalls = 0;
            auto numberOfOrderCopies = 0;
            auto numberOfMonResCopies = 0;
            storm::utility::Stopwatch loopWatch(true);

            if (!(useMonotonicity && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isDone() && regionQueue.top().localMonRes->getGlobalMonotonicityResult()->isAllMonotonicity())) {
                // Doing the extremal computation
                bool changed = false;

                auto totalArea = storm::utility::convertNumber<ConstantType>(region.area());
                auto coveredArea = storm::utility::zero<ConstantType>();
                while (!regionQueue.empty()) {
                    auto currRegion = regionQueue.top().region;
                    auto order = regionQueue.top().order;
                    auto localMonotonicityResult = regionQueue.top().localMonRes;
                    auto currBound = regionQueue.top().bound;
                    STORM_LOG_INFO("Currently looking at region: " << currRegion);

                    std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;

                    // Check whether this region needs further investigation based on the bound of the parent region
                    bool investigateBounds = !value
                                             || (minimize && currBound < value.get() - storm::utility::convertNumber<ConstantType>(precision))
                                             || (!minimize && currBound > value.get() + storm::utility::convertNumber<ConstantType>(precision));

                    if (investigateBounds) {
                        numberOfPLACalls++;
                        auto bounds = getBound(env, currRegion, dir, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
                        currBound = bounds[*this->parametricModel->getInitialStates().begin()];
                        // Check whether this region needs further investigation based on the bound of this region
                        bool lookAtRegion = !value
                                            || (minimize && currBound < value.get() - storm::utility::convertNumber<ConstantType>(precision))
                                            || (!minimize && currBound > value.get() + storm::utility::convertNumber<ConstantType>(precision));
                        if (lookAtRegion) {
                            if (useMonotonicity) {
                                // Continue extending order/monotonicity result
                                bool changedOrder = false;
                                if (!order->getDoneBuilding() && orderExtender->isHope(order, currRegion)) {
                                    if (numberOfCopiesOrder[order] != 1) {
                                        numberOfCopiesOrder[order]--;
                                        order = copyOrder(order);
                                        numberOfOrderCopies++;
                                    } else {
                                        assert (numberOfCopiesOrder[order] == 1);
                                    }
                                    this->extendOrder(env, order, currRegion);
                                    changedOrder = true;
                                }
                                if (changedOrder) {
                                    assert(!localMonotonicityResult->isDone());

                                    if (numberOfCopiesMonRes[localMonotonicityResult] != 1) {
                                        numberOfCopiesMonRes[localMonotonicityResult]--;
                                        localMonotonicityResult = localMonotonicityResult->copy();
                                        numberOfMonResCopies++;
                                    } else {
                                        assert (numberOfCopiesMonRes[localMonotonicityResult] == 1);
                                    }
                                    this->extendLocalMonotonicityResult(currRegion, order, localMonotonicityResult);
                                }
                            }

                            // Check whether this region contains a new 'good' value and set this value
                            auto point = useMonotonicity ? currRegion.getPoint(dir, *(localMonotonicityResult->getGlobalMonotonicityResult())) : currRegion.getCenterPoint();
                            auto currValue = getInstantiationChecker().check(env, point)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
                            if (!value || (minimize ? currValue <= value.get() : currValue >= value.get())) {
                                changed = true;
                                value = currValue;
                                valuation = point;
                            }

                            if ((minimize && currBound < value.get() - storm::utility::convertNumber<ConstantType>(precision))
                                || (!minimize && currBound > value.get() + storm::utility::convertNumber<ConstantType>(precision))) {
                                // We will split the region in this case, but first try to extend the order
                                if (useMonotonicity && this->isUseBoundsSet() && !order->getDoneBuilding()) {
                                    boundsWatch.start();
                                    numberOfPLACallsBounds++;
                                    if (minimize) {
                                        orderExtender->setMinValues(order, bounds);
                                        orderExtender->setMaxValues(order, getBound(env, currRegion, storm::solver::OptimizationDirection::Maximize, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                                    } else {
                                        orderExtender->setMaxValues(order, bounds);
                                        orderExtender->setMinValues(order, getBound(env, currRegion, storm::solver::OptimizationDirection::Minimize, localMonotonicityResult)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                                    }
                                    boundsWatch.stop();
                                    // We try to extend the order again based on minMaxValues
                                    auto i = order->getNumberOfDoneStates();
                                    this->extendOrder(env, order, currRegion);
                                    if (i < order->getNumberOfDoneStates()) {
                                        this->extendLocalMonotonicityResult(currRegion, order, localMonotonicityResult);
                                    }
                                }
                                // Now split the region
                                if (useMonotonicity) {
                                    this->splitSmart(currRegion, newRegions, order, *(localMonotonicityResult->getGlobalMonotonicityResult()), true);
                                } else if (this->isRegionSplitEstimateSupported()) {
                                    auto empty = storm::analysis::MonotonicityResult<VariableType>();
                                    this->splitSmart(currRegion, newRegions, order, empty, true);
                                } else {
                                    currRegion.split(currRegion.getCenterPoint(), newRegions);
                                }
                            }
                        }
                    }

                    // When the newRegions is empty we are done with the current region
                    if (newRegions.empty()) {
                        coveredArea += storm::utility::convertNumber<ConstantType>(currRegion.area());
                        if (order != nullptr) {
                            numberOfCopiesOrder[order]--;
                            numberOfCopiesMonRes[localMonotonicityResult]--;
                        }
                    } else {
                        STORM_LOG_INFO("Splitting region " << currRegion << " into " << newRegions.size());
                        numberOfSplits++;
                    }
                    regionQueue.pop();

                    // Add the new regions to the queue
                    if (useMonotonicity) {
                        for (auto &r : newRegions) {
                            r.setBoundParent(storm::utility::convertNumber<CoefficientType>(currBound));
                            regionQueue.emplace(r, order, localMonotonicityResult, currBound);
                        }
                        if (numberOfCopiesOrder.find(order) != numberOfCopiesOrder.end()) {
                            numberOfCopiesOrder[order] += newRegions.size();
                            numberOfCopiesMonRes[localMonotonicityResult] += newRegions.size();
                        } else {
                            numberOfCopiesOrder[order] = newRegions.size();
                            numberOfCopiesMonRes[localMonotonicityResult] = newRegions.size();
                        }
                    } else {
                        for (auto &r : newRegions) {
                            r.setBoundParent(storm::utility::convertNumber<CoefficientType>(currBound));
                            regionQueue.emplace(r, nullptr, nullptr, currBound);
                        }
                    }

                    STORM_LOG_INFO("Current value : " << value.get() << ", current bound: " << currBound << ".");
                    STORM_LOG_INFO("Covered " << (coveredArea * storm::utility::convertNumber<ConstantType>(100.0) / totalArea) << "% of the region." << std::endl);
                }
                loopWatch.stop();
            }

            STORM_PRINT("Total number of splits: " << numberOfSplits << std::endl);
            STORM_PRINT("Total number of plaCalls: " << numberOfPLACalls << std::endl);
            if (useMonotonicity) {
                STORM_PRINT("Total number of plaCalls for bounds for monotonicity checking: " << numberOfPLACallsBounds << std::endl);
                STORM_PRINT("Total number of copies of the order: " << numberOfOrderCopies << std::endl);
                STORM_PRINT("Total number of copies of the local monotonicity result: " << numberOfMonResCopies
                                                                                << std::endl);
            }
            STORM_PRINT(std::endl << "Total time for region refinement: " << loopWatch << "." << std::endl << std::endl);
            STORM_PRINT(std::endl << "Total time for additional bounds: " << boundsWatch << "." << std::endl << std::endl);

            return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value.get()), valuation);
        }

        template<typename SparseModelType, typename ConstantType>
        std::pair<typename SparseModelType::ValueType, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getGoodInitialPoint(const Environment &env, const storage::ParameterRegion<typename SparseModelType::ValueType> &region, const OptimizationDirection &dir, std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonRes) {
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::Valuation Valuation;
            typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
            ConstantType value = storm::solver::minimize(dir) ? 1 : 0;
            Valuation valuation;
            std::set<VariableType> monIncr, monDecr, notMon, notMonFirst;

            if (localMonRes != nullptr) {
                localMonRes->getGlobalMonotonicityResult()->splitBasedOnMonotonicity(region.getVariables(), monIncr, monDecr, notMonFirst);

                auto numMon = monIncr.size() + monDecr.size();
                STORM_PRINT("Number of monotone parameters: " << numMon << std::endl;);

                if (numMon < region.getVariables().size()) {
                    checkForPossibleMonotonicity(env, region, monIncr, monDecr, notMon, notMonFirst, dir);
                    STORM_PRINT("Number of possible monotone parameters: " << (monIncr.size() + monDecr.size() - numMon) << std::endl;);
                    STORM_PRINT("Number of definitely not monotone parameters: " << notMon.size() << std::endl;);
                }

                valuation = region.getPoint(dir, monIncr, monDecr);
//                std::size_t const numOfSamples = 50;
//                std::vector<Valuation> resultingVector(numOfSamples);
//                std::map<VariableType, CoefficientType> stepSize;
//                for (auto variable: notMon) {
//                    stepSize[variable] = (region.getUpperBoundary(variable) - region.getLowerBoundary(variable)) / (numOfSamples - 1);
//                }
//
//                for (uint_fast64_t i = 0; i < numOfSamples; ++i) {
//                    for (auto variable : notMon) {
//                        resultingVector[i].insert(std::pair<VariableType, CoefficientType>(variable, (region.getLowerBoundary(variable) + stepSize[variable] * i)));
//                    }
//                    for (auto variable: monIncr) {
//                        if (storm::solver::minimize(dir)) {
//                            resultingVector[i].insert(std::pair<VariableType, CoefficientType>(variable, region.getLowerBoundary(variable)));
//                        } else {
//                            resultingVector[i].insert(std::pair<VariableType, CoefficientType>(variable, region.getUpperBoundary(variable)));
//                        }
//                    }
//                    for (auto variable : monDecr) {
//                        if (!storm::solver::minimize(dir)) {
//                            resultingVector[i].insert(std::pair<VariableType, CoefficientType>(variable, region.getLowerBoundary(variable)));
//                        } else {
//                            resultingVector[i].insert(std::pair<VariableType, CoefficientType>(variable, region.getUpperBoundary(variable)));
//                        }
//                    }
//                }
//
//                for (auto &point : resultingVector) {
//                    auto currValue = getInstantiationChecker().check(env, point)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];
//                    if (storm::solver::minimize(dir) ? currValue <= value : currValue >= value) {
//                        value = currValue;
//                        valuation = point;
//                    }
//                }
            } else {
                valuation = region.getCenterPoint();
            }
            value = getInstantiationChecker().check(env, valuation)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()];

            return std::make_pair(storm::utility::convertNumber<typename SparseModelType::ValueType>(value), std::move(valuation));
        }

        template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
        template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
        template class SparseParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
        template class SparseParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
    }
}


text:
#include "common.h"
#include "shared_data.h"
#include "io_service_pool.h"
#include "xdaemon.h"
#include "args.h"

#include <boost/algorithm/string.hpp>
#include <list>

using namespace std;

namespace proxy_ns
{

class ProxyServer
{
public:
	ProxyServer()
	{
		sdata.init();
	}

	~ProxyServer()
	{
		LDebug("");
		args.running_flag = false;
		sdata.stop();
	}

	void run()
	{
		args.running_flag = true;
		sdata.start();

		{
			global::xrecursive_mutex::scoped_lock lock(global::exit_mtx);
			global::exit_condition.wait(global::exit_mtx);
		}
		args.running_flag = false;

	}

private:

};

}

int main(int ac, char* av[])
try
{
	using namespace proxy_ns;
	global::ServerInfo::instance().init("proxy", "faraway_proxy", "faraway_proxy 1.0.000");
	args.init(ac, av);

	LNotice("faraway_proxy launched");
	ProxyServer server;
	server.run();
	LNotice("faraway_proxy stoped");
}
catch(global::trackerr& e)
{
	LErrStr(boost::format("faraway_proxy fail, an error occured: %s") % e.what());
	return 1;
}
catch(std::exception& e)
{
	LErrStr(boost::format("faraway_proxy fail, an error occured: %s") % e.what());
	return 1;
}
catch(...)
{
	LErr("faraway_proxy fail, an unknown error occured");
	return 1;
}

max_stars_repo_name: netaudio/TCP-UDP-Proxy

max_issues_repo_name: netaudio/TCP-UDP-Proxy

max_forks_repo_name: netaudio/TCP-UDP-Proxy


text:
#if !defined(BOOST_PROTO_DONT_USE_PREPROCESSED_FILES)

#include <boost/proto/detail/preprocessed/template_arity_helper.hpp>

#elif !defined(BOOST_PP_IS_ITERATING)

#if defined(__WAVE__) && defined(BOOST_PROTO_CREATE_PREPROCESSED_FILES)
#pragma wave option(preserve : 2, line : 0, output                             \
                    : "preprocessed/template_arity_helper.hpp")
#endif

///////////////////////////////////////////////////////////////////////////////
// template_arity_helper.hpp
// Overloads of template_arity_helper, used by the template_arity\<\> class
// template
//
//  Copyright 2008 Eric Niebler. Distributed under the Boost
//  Software License, Version 1.0. (See accompanying file
//  LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)

#if defined(__WAVE__) && defined(BOOST_PROTO_CREATE_PREPROCESSED_FILES)
#pragma wave option(preserve : 1)
#endif

#define BOOST_PP_ITERATION_PARAMS_1                                            \
  (3, (1, BOOST_PROTO_MAX_ARITY,                                               \
       <boost / proto / detail / template_arity_helper.hpp>))
#include BOOST_PP_ITERATE()

#if defined(__WAVE__) && defined(BOOST_PROTO_CREATE_PREPROCESSED_FILES)
#pragma wave option(output : null)
#endif

#else

#define N BOOST_PP_ITERATION()

template <template <BOOST_PP_ENUM_PARAMS(N, typename P)> class F,
          BOOST_PP_ENUM_PARAMS(N, typename T)>
sized_type<BOOST_PP_INC(N)>::type
template_arity_helper(F<BOOST_PP_ENUM_PARAMS(N, T)> **, mpl::int_<N> *);

#undef N

#endif // BOOST_PROTO_DONT_USE_PREPROCESSED_FILES

ext: hpp

max_stars_repo_name: henrywarhurst/matrix

max_issues_repo_name: henrywarhurst/matrix

max_forks_repo_name: henrywarhurst/matrix


text: #include <boost/asio/placeholders.hpp>

max_stars_repo_name: miathedev/BoostForArduino

max_issues_repo_name: miathedev/BoostForArduino

max_forks_repo_name: miathedev/BoostForArduino


text:
// *****************************************************************************
/*!
  \file      src/NoWarning/value_factory.hpp
  \copyright 2012-2015 J. Bakosi,
             2016-2018 Los Alamos National Security, LLC.,
             2019 Triad National Security, LLC.
             All rights reserved. See the LICENSE file for details.
  \brief     Include boost/functional/value_factory.hpp with turning off
             specific compiler warnings
*/
// *****************************************************************************
#ifndef nowarning_value_factory_h
#define nowarning_value_factory_h

#include "Macro.hpp"

#if defined(__clang__)
  #pragma clang diagnostic push
  #pragma clang diagnostic ignored "-Wsign-conversion"
#elif defined(STRICT_GNUC)
  #pragma GCC diagnostic push
  #pragma GCC diagnostic ignored "-Wstrict-aliasing"
#endif

#include <boost/functional/value_factory.hpp>

#if defined(__clang__)
  #pragma clang diagnostic pop
#elif defined(STRICT_GNUC)
  #pragma GCC diagnostic pop
#endif

#endif // nowarning_value_factory_h

max_stars_repo_name: franjgonzalez/Quinoa

max_issues_repo_name: franjgonzalez/Quinoa

max_forks_repo_name: franjgonzalez/Quinoa