formulas.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/tl/formula.hh>
 
namespace spot
{
  namespace gen
  {
 
    enum ltl_pattern_id {
      LTL_BEGIN = 256,
      LTL_AND_F = LTL_BEGIN,
      LTL_AND_FG,
      LTL_AND_GF,
      LTL_CCJ_ALPHA,
      LTL_CCJ_BETA,
      LTL_CCJ_BETA_PRIME,
      LTL_DAC_PATTERNS,
      LTL_EH_PATTERNS,
      LTL_EIL_GSI,
      LTL_FXG_OR,
      LTL_GF_EQUIV,
      LTL_GF_EQUIV_XN,
      LTL_GF_IMPLIES,
      LTL_GF_IMPLIES_XN,
      LTL_GH_Q,
      LTL_GH_R,
      LTL_GO_THETA,
      LTL_GXF_AND,
      LTL_HKRSS_PATTERNS,
      LTL_KR_N,
      LTL_KR_NLOGN,
      LTL_KV_PSI,
      LTL_MS_EXAMPLE,
      LTL_MS_PHI_H,
      LTL_MS_PHI_R,
      LTL_MS_PHI_S,
      LTL_OR_FG,
      LTL_OR_G,
      LTL_OR_GF,
      LTL_P_PATTERNS,
      LTL_PPS_ARBITER_STANDARD,
      LTL_PPS_ARBITER_STRICT,
      LTL_R_LEFT,
      LTL_R_RIGHT,
      LTL_RV_COUNTER,
      LTL_RV_COUNTER_CARRY,
      LTL_RV_COUNTER_CARRY_LINEAR,
      LTL_RV_COUNTER_LINEAR,
      LTL_SB_PATTERNS,
      LTL_SEJK_F,
      LTL_SEJK_J,
      LTL_SEJK_K,
      LTL_SEJK_PATTERNS,
      LTL_TV_F1,
      LTL_TV_F2,
      LTL_TV_G1,
      LTL_TV_G2,
      LTL_TV_UU,
      LTL_U_LEFT,
      LTL_U_RIGHT,
      LTL_END
    };
 
    SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n, int m = -1);
 
    SPOT_API const char* ltl_pattern_name(ltl_pattern_id pattern);
 
    SPOT_API int ltl_pattern_max(ltl_pattern_id pattern);
 
    SPOT_API int ltl_pattern_argc(ltl_pattern_id pattern);
  }
}