Replace guards by pragma once.
* iface/ltsmin/ltsmin.hh, src/bin/common_aoutput.hh, src/bin/common_conv.hh, src/bin/common_cout.hh, src/bin/common_file.hh, src/bin/common_finput.hh, src/bin/common_output.hh, src/bin/common_post.hh, src/bin/common_r.hh, src/bin/common_range.hh, src/bin/common_setup.hh, src/bin/common_sys.hh, src/bin/common_trans.hh, src/dstarparse/parsedecl.hh, src/dstarparse/public.hh, src/graph/graph.hh, src/graph/ngraph.hh, src/hoaparse/parsedecl.hh, src/hoaparse/public.hh, src/kripke/fairkripke.hh, src/kripke/fwd.hh, src/kripke/kripke.hh, src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.hh, src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh, src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/ltlvisit/apcollect.hh, src/ltlvisit/clone.hh, src/ltlvisit/contain.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/lbt.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.hh, src/ltlvisit/mutation.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh, src/ltlvisit/relabel.hh, src/ltlvisit/remove_x.hh, src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh, src/ltlvisit/tostring.hh, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.hh, src/misc/bareword.hh, src/misc/bddlt.hh, src/misc/bitvect.hh, src/misc/casts.hh, src/misc/common.hh, src/misc/escape.hh, src/misc/fixpool.hh, src/misc/formater.hh, src/misc/hash.hh, src/misc/hashfunc.hh, src/misc/intvcmp2.hh, src/misc/intvcomp.hh, src/misc/location.hh, src/misc/ltstr.hh, src/misc/memusage.hh, src/misc/minato.hh, src/misc/mspool.hh, src/misc/optionmap.hh, src/misc/position.hh, src/misc/random.hh, src/misc/satsolver.hh, src/misc/timer.hh, src/misc/tmpfile.hh, src/misc/version.hh, src/priv/accmap.hh, src/priv/bddalloc.hh, src/priv/freelist.hh, src/ta/ta.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.hh, src/taalgos/emptinessta.hh, src/taalgos/minimize.hh, src/taalgos/reachiter.hh, src/taalgos/statessetbuilder.hh, src/taalgos/stats.hh, src/taalgos/tgba2ta.hh, src/tgba/acc.hh, src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/formula2bdd.hh, src/tgba/fwd.hh, src/tgba/taatgba.hh, src/tgba/tgba.hh, src/tgba/tgbagraph.hh, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/bfssteps.hh, src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh, src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.hh, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/product.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh, src/tgbaalgos/remfin.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/safety.hh, src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh, src/tgbaalgos/stutter.hh, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh, src/tgbaalgos/weight.hh, src/tgbaalgos/word.hh, src/sanity/includes.test, src/tgbaalgos/ndfs_result.hxx: here.
This commit is contained in:
Etienne Renault
parent
b8bc619ddf
commit
57cd9f2d2c
172 changed files with 352 additions and 946 deletions
|
|
@ -17,14 +17,12 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_IFACE_LTSMIN_LTSMIN_HH
|
||||
# define SPOT_IFACE_LTSMIN_LTSMIN_HH
|
||||
#pragma once
|
||||
|
||||
#include "kripke/kripke.hh"
|
||||
#include "ltlvisit/apcollect.hh"
|
||||
#include "ltlast/constant.hh"
|
||||
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
|
|
@ -64,5 +62,3 @@ namespace spot
|
|||
const ltl::formula* dead = ltl::constant::true_instance(),
|
||||
int compress = 0, bool verbose = true);
|
||||
}
|
||||
|
||||
#endif // SPOT_IFACE_LTSMIN_LTSMIN_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_AOUTPUT_HH
|
||||
#define SPOT_BIN_COMMON_AOUTPUT_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
|
||||
|
|
@ -237,7 +236,3 @@ public:
|
|||
|
||||
void add_stat(char c, const spot::printable* p);
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_AOUTPUT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_CONV_HH
|
||||
#define SPOT_BIN_COMMON_CONV_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include "tgba/tgbagraph.hh"
|
||||
|
|
@ -34,6 +33,3 @@ std::vector<long> to_longs(const char* s);
|
|||
|
||||
spot::tgba_digraph_ptr
|
||||
read_automaton(const char* filename, spot::bdd_dict_ptr& dict);
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_CONV_HH
|
||||
|
|
|
|||
|
|
@ -17,10 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_COUT_HH
|
||||
#define SPOT_BIN_COMMON_COUT_HH
|
||||
#pragma once
|
||||
|
||||
void check_cout();
|
||||
void flush_cout();
|
||||
|
||||
#endif // SPOT_BIN_COMMON_COUT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_FILE_HH
|
||||
#define SPOT_BIN_COMMON_FILE_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include <iosfwd>
|
||||
|
|
@ -50,5 +49,3 @@ public:
|
|||
return *os_;
|
||||
}
|
||||
};
|
||||
|
||||
#endif // SPOT_BIN_COMMON_FILE_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_FINPUT_HH
|
||||
#define SPOT_BIN_COMMON_FINPUT_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
|
||||
|
|
@ -79,7 +78,3 @@ public:
|
|||
char* prefix;
|
||||
char* suffix;
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_FINPUT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_OUTPUT_HH
|
||||
#define SPOT_BIN_COMMON_OUTPUT_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
|
||||
|
|
@ -83,5 +82,3 @@ public:
|
|||
|
||||
printable_formula formula_;
|
||||
};
|
||||
|
||||
#endif // SPOT_BIN_COMMON_OUTPUT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_POST_HH
|
||||
#define SPOT_BIN_COMMON_POST_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include "tgbaalgos/postproc.hh"
|
||||
|
|
@ -31,7 +30,3 @@ extern spot::postprocessor::output_type type;
|
|||
extern spot::postprocessor::output_pref pref;
|
||||
extern spot::postprocessor::output_pref comp;
|
||||
extern spot::postprocessor::optimization_level level;
|
||||
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_FINPUT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_R_HH
|
||||
#define SPOT_BIN_COMMON_R_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
|
|
@ -45,5 +44,3 @@ extern int simplification_level;
|
|||
|
||||
void parse_r(const char* arg);
|
||||
spot::ltl::ltl_simplifier_options simplifier_options();
|
||||
|
||||
#endif // SPOT_BIN_COMMON_RANGE_HH
|
||||
|
|
|
|||
|
|
@ -17,9 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_RANGE_HH
|
||||
#define SPOT_BIN_COMMON_RANGE_HH
|
||||
|
||||
#pragma once
|
||||
|
||||
#define RANGE_DOC \
|
||||
{ 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', " \
|
||||
|
|
@ -48,5 +46,3 @@ struct range
|
|||
// is disallowed.
|
||||
range parse_range(const char* str,
|
||||
int missing_left = 1, int missing_right = 0);
|
||||
|
||||
#endif // SPOT_BIN_COMMON_RANGE_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_SETUP_HH
|
||||
#define SPOT_BIN_COMMON_SETUP_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include "progname.h"
|
||||
|
|
@ -27,5 +26,3 @@ void setup(char** progname);
|
|||
|
||||
extern const struct argp misc_argp;
|
||||
extern const struct argp misc_argp_hidden;
|
||||
|
||||
#endif // SPOT_BIN_COMMON_SETUP_HH
|
||||
|
|
|
|||
|
|
@ -17,11 +17,8 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_SYS_HH
|
||||
#define SPOT_BIN_COMMON_SYS_HH
|
||||
#pragma once
|
||||
|
||||
#ifdef HAVE_CONFIG_H
|
||||
# include "config.h"
|
||||
#endif
|
||||
|
||||
#endif // SPOT_BIN_COMMON_SYS_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_TRANS_HH
|
||||
#define SPOT_BIN_COMMON_TRANS_HH
|
||||
#pragma once
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include <vector>
|
||||
|
|
@ -118,6 +117,3 @@ int exec_with_timeout(const char* cmd);
|
|||
#define exec_with_timeout(cmd) system(cmd)
|
||||
#define setup_sig_handler() while (0);
|
||||
#endif // !ENABLE_TIMEOUT
|
||||
|
||||
|
||||
#endif // SPOT_BIN_COMMON_TRANS_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_DSTARPARSE_PARSEDECL_HH
|
||||
# define SPOT_DSTARPARSE_PARSEDECL_HH
|
||||
#pragma once
|
||||
|
||||
#include <string>
|
||||
#include "dstarparse.hh"
|
||||
|
|
@ -35,5 +34,3 @@ namespace spot
|
|||
int dstaryyopen(const std::string& name);
|
||||
void dstaryyclose();
|
||||
}
|
||||
|
||||
#endif // SPOT_DSTARPARSE_PARSEDECL_HH
|
||||
|
|
|
|||
|
|
@ -17,17 +17,16 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_DSTARPARSE_PUBLIC_HH
|
||||
# define SPOT_DSTARPARSE_PUBLIC_HH
|
||||
#pragma once
|
||||
|
||||
# include "tgba/tgbagraph.hh"
|
||||
# include "misc/location.hh"
|
||||
# include "ltlenv/defaultenv.hh"
|
||||
# include <string>
|
||||
# include <list>
|
||||
# include <utility>
|
||||
# include <iosfwd>
|
||||
# include <misc/bitvect.hh>
|
||||
#include "tgba/tgbagraph.hh"
|
||||
#include "misc/location.hh"
|
||||
#include "ltlenv/defaultenv.hh"
|
||||
#include <string>
|
||||
#include <list>
|
||||
#include <utility>
|
||||
#include <iosfwd>
|
||||
#include <misc/bitvect.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -147,8 +146,5 @@ namespace spot
|
|||
SPOT_API tgba_digraph_ptr
|
||||
dstar_to_tgba(const const_dstar_aut_ptr& dstar);
|
||||
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_DSTARPARSE_PUBLIC_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_GRAPH_GRAPH_HH
|
||||
# define SPOT_GRAPH_GRAPH_HH
|
||||
#pragma once
|
||||
|
||||
#include "misc/common.hh"
|
||||
#include <vector>
|
||||
|
|
@ -959,9 +958,5 @@ namespace spot
|
|||
//std::cerr << "\nafter defrag\n";
|
||||
//dump_storage(std::cerr);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_GRAPH_GRAPH_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_GRAPH_NGRAPH_HH
|
||||
# define SPOT_GRAPH_NGRAPH_HH
|
||||
#pragma once
|
||||
|
||||
#include <unordered_map>
|
||||
#include <vector>
|
||||
|
|
@ -162,7 +161,4 @@ namespace spot
|
|||
return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_GRAPH_NGRAPH_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_HOAPARSE_PARSEDECL_HH
|
||||
# define SPOT_HOAPARSE_PARSEDECL_HH
|
||||
#pragma once
|
||||
|
||||
#include <string>
|
||||
#include "hoaparse.hh"
|
||||
|
|
@ -42,5 +41,3 @@ namespace spot
|
|||
spot::location pos;
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_HOAPARSE_PARSEDECL_HH
|
||||
|
|
|
|||
|
|
@ -17,17 +17,16 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_HOAPARSE_PUBLIC_HH
|
||||
# define SPOT_HOAPARSE_PUBLIC_HH
|
||||
#pragma once
|
||||
|
||||
# include "tgba/tgbagraph.hh"
|
||||
# include "misc/location.hh"
|
||||
# include "ltlenv/defaultenv.hh"
|
||||
# include <string>
|
||||
# include <list>
|
||||
# include <utility>
|
||||
# include <iosfwd>
|
||||
# include <misc/bitvect.hh>
|
||||
#include "tgba/tgbagraph.hh"
|
||||
#include "misc/location.hh"
|
||||
#include "ltlenv/defaultenv.hh"
|
||||
#include <string>
|
||||
#include <list>
|
||||
#include <utility>
|
||||
#include <iosfwd>
|
||||
#include <misc/bitvect.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -130,5 +129,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_HOAPARSE_PUBLIC_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_KRIPKE_FAIRKRIPKE_HH
|
||||
# define SPOT_KRIPKE_FAIRKRIPKE_HH
|
||||
#pragma once
|
||||
|
||||
#include "tgba/tgba.hh"
|
||||
#include "fwd.hh"
|
||||
|
|
@ -106,8 +105,4 @@ namespace spot
|
|||
protected:
|
||||
virtual bdd compute_support_conditions(const state* s) const;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_KRIPKE_FAIRKRIPKE_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_KRIPKE_FWD_HH
|
||||
# define SPOT_KRIPKE_FWD_HH
|
||||
#pragma once
|
||||
|
||||
#include <memory>
|
||||
|
||||
|
|
@ -36,5 +35,3 @@ namespace spot
|
|||
typedef std::shared_ptr<const kripke_explicit> const_kripke_explicit_ptr;
|
||||
typedef std::shared_ptr<kripke_explicit> kripke_explicit_ptr;
|
||||
}
|
||||
|
||||
#endif // SPOT_KRIPKE_FWD_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_KRIPKE_KRIPKE_HH
|
||||
# define SPOT_KRIPKE_KRIPKE_HH
|
||||
#pragma once
|
||||
|
||||
#include "fairkripke.hh"
|
||||
|
||||
|
|
@ -97,15 +96,11 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
|
||||
virtual ~kripke();
|
||||
|
||||
virtual acc_cond::mark_t state_acceptance_conditions(const state*) const;
|
||||
};
|
||||
|
||||
|
||||
typedef std::shared_ptr<kripke> kripke_ptr;
|
||||
typedef std::shared_ptr<const kripke> const_kripke_ptr;
|
||||
}
|
||||
|
||||
#endif // SPOT_KRIPKE_KRIPKE_HH
|
||||
|
|
|
|||
|
|
@ -17,14 +17,12 @@
|
|||
// 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
|
||||
|
||||
#ifndef SPOT_KRIPKE_KRIPKEEXPLICIT_HH
|
||||
# define SPOT_KRIPKE_KRIPKEEXPLICIT_HH
|
||||
|
||||
# include <iosfwd>
|
||||
# include "kripke.hh"
|
||||
# include "ltlast/formula.hh"
|
||||
# include "kripkeprint.hh"
|
||||
#include <iosfwd>
|
||||
#include "kripke.hh"
|
||||
#include "ltlast/formula.hh"
|
||||
#include "kripkeprint.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -185,4 +183,3 @@ namespace spot
|
|||
return std::make_shared<kripke_explicit>(d, init);
|
||||
}
|
||||
}
|
||||
#endif // SPOT_KRIPKE_KRIPKEEXPLICIT_HH
|
||||
|
|
|
|||
|
|
@ -17,13 +17,11 @@
|
|||
// 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
|
||||
|
||||
#ifndef SPOT_KRIPKE_KRIPKEPRINT_HH
|
||||
# define SPOT_KRIPKE_KRIPKEPRINT_HH
|
||||
|
||||
# include "misc/common.hh"
|
||||
# include <iosfwd>
|
||||
# include "kripke.hh"
|
||||
#include "misc/common.hh"
|
||||
#include <iosfwd>
|
||||
#include "kripke.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -52,5 +50,3 @@ namespace spot
|
|||
kripke_save_reachable_renumbered(std::ostream& os, const const_kripke_ptr& k);
|
||||
|
||||
} // End namespace spot
|
||||
|
||||
#endif // SPOT_KRIPKE_KRIPKEPRINT_HH
|
||||
|
|
|
|||
|
|
@ -18,12 +18,11 @@
|
|||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#ifndef SPOT_KRIPKEPARSE_PARSEDECL_HH
|
||||
# define SPOT_KRIPKEPARSE_PARSEDECL_HH
|
||||
#pragma once
|
||||
|
||||
# include <string>
|
||||
# include "kripkeparse.hh"
|
||||
# include "misc/location.hh"
|
||||
#include <string>
|
||||
#include "kripkeparse.hh"
|
||||
#include "misc/location.hh"
|
||||
|
||||
# define YY_DECL \
|
||||
int kripkeyylex (kripkeyy::parser::semantic_type *yylval, \
|
||||
|
|
@ -36,5 +35,3 @@ namespace spot
|
|||
int kripkeyyopen(const std::string& name);
|
||||
void kripkeyyclose();
|
||||
}
|
||||
|
||||
#endif /* !PARSEDECL_HH_ */
|
||||
|
|
|
|||
|
|
@ -17,17 +17,15 @@
|
|||
// 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
|
||||
|
||||
#ifndef SPOT_KRIPKEPARSE_PUBLIC_HH
|
||||
# define SPOT_KRIPKEPARSE_PUBLIC_HH
|
||||
|
||||
# include "kripke/kripkeexplicit.hh"
|
||||
# include "misc/location.hh"
|
||||
# include "ltlenv/defaultenv.hh"
|
||||
# include <string>
|
||||
# include <list>
|
||||
# include <utility>
|
||||
# include <iosfwd>
|
||||
#include "kripke/kripkeexplicit.hh"
|
||||
#include "misc/location.hh"
|
||||
#include "ltlenv/defaultenv.hh"
|
||||
#include <string>
|
||||
#include <list>
|
||||
#include <utility>
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -58,8 +56,4 @@ namespace spot
|
|||
bool format_kripke_parse_errors(std::ostream& os,
|
||||
const std::string& filename,
|
||||
kripke_parse_error_list& error_list);
|
||||
|
||||
}
|
||||
|
||||
|
||||
#endif /* !SPOT_KRIPKEPARSE_PUBLIC_HH_ */
|
||||
|
|
|
|||
|
|
@ -26,14 +26,11 @@
|
|||
/// This file is usually needed when \b defining a visitor.
|
||||
/// Prefer ltlast/predecl.hh when only \b declaring methods and functions
|
||||
/// over LTL nodes.
|
||||
#ifndef SPOT_LTLAST_ALLNODES_HH
|
||||
# define SPOT_LTLAST_ALLNODES_HH
|
||||
#pragma once
|
||||
|
||||
# include "binop.hh"
|
||||
# include "unop.hh"
|
||||
# include "multop.hh"
|
||||
# include "atomic_prop.hh"
|
||||
# include "constant.hh"
|
||||
# include "bunop.hh"
|
||||
|
||||
#endif // SPOT_LTLAST_ALLNODES_HH
|
||||
#include "binop.hh"
|
||||
#include "unop.hh"
|
||||
#include "multop.hh"
|
||||
#include "atomic_prop.hh"
|
||||
#include "constant.hh"
|
||||
#include "bunop.hh"
|
||||
|
|
|
|||
|
|
@ -22,8 +22,7 @@
|
|||
|
||||
/// \file ltlast/atomic_prop.hh
|
||||
/// \brief LTL atomic propositions
|
||||
#ifndef SPOT_LTLAST_ATOMIC_PROP_HH
|
||||
# define SPOT_LTLAST_ATOMIC_PROP_HH
|
||||
#pragma once
|
||||
|
||||
#include "formula.hh"
|
||||
#include <string>
|
||||
|
|
@ -91,5 +90,3 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_ATOMICPROP_HH
|
||||
|
|
|
|||
|
|
@ -25,8 +25,7 @@
|
|||
///
|
||||
/// This does not include \c AND and \c OR operators. These are
|
||||
/// considered to be multi-operand operators (see spot::ltl::multop).
|
||||
#ifndef SPOT_LTLAST_BINOP_HH
|
||||
# define SPOT_LTLAST_BINOP_HH
|
||||
#pragma once
|
||||
|
||||
#include "formula.hh"
|
||||
#include <map>
|
||||
|
|
@ -238,5 +237,3 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_BINOP_HH
|
||||
|
|
|
|||
|
|
@ -19,8 +19,7 @@
|
|||
|
||||
/// \file ltlast/bunop.hh
|
||||
/// \brief Bounded Unary operators
|
||||
#ifndef SPOT_LTLAST_BUNOP_HH
|
||||
# define SPOT_LTLAST_BUNOP_HH
|
||||
#pragma once
|
||||
|
||||
#include "formula.hh"
|
||||
#include <map>
|
||||
|
|
@ -215,4 +214,3 @@ namespace spot
|
|||
|
||||
}
|
||||
}
|
||||
#endif // SPOT_LTLAST_BUNOP_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
|
||||
/// \file ltlast/constant.hh
|
||||
/// \brief LTL constants
|
||||
#ifndef SPOT_LTLAST_CONSTANT_HH
|
||||
# define SPOT_LTLAST_CONSTANT_HH
|
||||
#pragma once
|
||||
|
||||
#include "formula.hh"
|
||||
|
||||
|
|
@ -85,5 +84,3 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_CONSTANT_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
|
||||
/// \file ltlast/formula.hh
|
||||
/// \brief LTL formula interface
|
||||
#ifndef SPOT_LTLAST_FORMULA_HH
|
||||
# define SPOT_LTLAST_FORMULA_HH
|
||||
#pragma once
|
||||
|
||||
#include "misc/common.hh"
|
||||
#include <string>
|
||||
|
|
@ -533,5 +532,3 @@ namespace std
|
|||
};
|
||||
}
|
||||
#endif
|
||||
|
||||
#endif // SPOT_LTLAST_FORMULA_HH
|
||||
|
|
|
|||
|
|
@ -22,8 +22,7 @@
|
|||
|
||||
/// \file ltlast/multop.hh
|
||||
/// \brief LTL multi-operand operators
|
||||
#ifndef SPOT_LTLAST_MULTOP_HH
|
||||
# define SPOT_LTLAST_MULTOP_HH
|
||||
#pragma once
|
||||
|
||||
#include "formula.hh"
|
||||
#include <vector>
|
||||
|
|
@ -317,5 +316,3 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_MULTOP_HH
|
||||
|
|
|
|||
|
|
@ -27,8 +27,7 @@
|
|||
/// over LTL nodes.
|
||||
/// Use ltlast/allnodes.hh or an individual header when the definition of
|
||||
/// the node is actually needed.
|
||||
#ifndef SPOT_LTLAST_PREDECL_HH
|
||||
# define SPOT_LTLAST_PREDECL_HH
|
||||
#pragma once
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -45,5 +44,3 @@ namespace spot
|
|||
class unop;
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_PREDECL_HH
|
||||
|
|
|
|||
|
|
@ -22,8 +22,7 @@
|
|||
|
||||
/// \file ltlast/unop.hh
|
||||
/// \brief LTL unary operators
|
||||
#ifndef SPOT_LTLAST_UNOP_HH
|
||||
# define SPOT_LTLAST_UNOP_HH
|
||||
#pragma once
|
||||
|
||||
#include <map>
|
||||
#include <iosfwd>
|
||||
|
|
@ -217,5 +216,3 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_UNOP_HH
|
||||
|
|
|
|||
|
|
@ -22,11 +22,10 @@
|
|||
|
||||
/// \file ltlast/visitor.hh
|
||||
/// \brief LTL visitor interface
|
||||
#ifndef SPOT_LTLAST_VISITOR_HH
|
||||
# define SPOT_LTLAST_VISITOR_HH
|
||||
#pragma once
|
||||
|
||||
# include "misc/common.hh"
|
||||
# include "predecl.hh"
|
||||
#include "misc/common.hh"
|
||||
#include "predecl.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -50,5 +49,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLAST_VISITOR_HH
|
||||
|
|
|
|||
|
|
@ -20,13 +20,12 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLENV_DECLENV_HH
|
||||
# define SPOT_LTLENV_DECLENV_HH
|
||||
#pragma once
|
||||
|
||||
# include "environment.hh"
|
||||
# include <string>
|
||||
# include <map>
|
||||
# include "ltlast/atomic_prop.hh"
|
||||
#include "environment.hh"
|
||||
#include <string>
|
||||
#include <map>
|
||||
#include "ltlast/atomic_prop.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -63,5 +62,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLENV_DECLENV_HH
|
||||
|
|
|
|||
|
|
@ -20,11 +20,10 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLENV_DEFAULTENV_HH
|
||||
# define SPOT_LTLENV_DEFAULTENV_HH
|
||||
#pragma once
|
||||
|
||||
# include "environment.hh"
|
||||
# include "ltlast/atomic_prop.hh"
|
||||
#include "environment.hh"
|
||||
#include "ltlast/atomic_prop.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -50,8 +49,5 @@ namespace spot
|
|||
protected:
|
||||
default_environment();
|
||||
};
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLENV_DEFAULTENV_HH
|
||||
|
|
|
|||
|
|
@ -20,11 +20,10 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLENV_ENVIRONMENT_HH
|
||||
# define SPOT_LTLENV_ENVIRONMENT_HH
|
||||
#pragma once
|
||||
|
||||
# include "ltlast/formula.hh"
|
||||
# include <string>
|
||||
#include "ltlast/formula.hh"
|
||||
#include <string>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -65,5 +64,3 @@ namespace spot
|
|||
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLENV_ENVIRONMENT_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLPARSE_PARSEDECL_HH
|
||||
# define SPOT_LTLPARSE_PARSEDECL_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlparse.hh"
|
||||
#include "misc/location.hh"
|
||||
|
|
@ -34,5 +33,3 @@ YY_DECL;
|
|||
|
||||
void flex_set_buffer(const std::string& buf, int start_tok, bool lenient);
|
||||
void flex_unset_buffer();
|
||||
|
||||
#endif // SPOT_LTLPARSE_PARSEDECL_HH
|
||||
|
|
|
|||
|
|
@ -20,16 +20,15 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLPARSE_PUBLIC_HH
|
||||
# define SPOT_LTLPARSE_PUBLIC_HH
|
||||
#pragma once
|
||||
|
||||
# include "ltlast/formula.hh"
|
||||
# include "misc/location.hh"
|
||||
# include "ltlenv/defaultenv.hh"
|
||||
# include <string>
|
||||
# include <list>
|
||||
# include <utility>
|
||||
# include <iosfwd>
|
||||
#include "ltlast/formula.hh"
|
||||
#include "misc/location.hh"
|
||||
#include "ltlenv/defaultenv.hh"
|
||||
#include <string>
|
||||
#include <list>
|
||||
#include <utility>
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -217,5 +216,3 @@ namespace spot
|
|||
/// @}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLPARSE_PUBLIC_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_APCOLLECT_HH
|
||||
# define SPOT_LTLVISIT_APCOLLECT_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/atomic_prop.hh"
|
||||
#include <set>
|
||||
|
|
@ -74,4 +73,3 @@ namespace spot
|
|||
/// @}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_CLONE_HH
|
||||
# define SPOT_LTLVISIT_CLONE_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "ltlast/visitor.hh"
|
||||
|
|
@ -59,5 +58,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_LUNABBREV_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_CONTAIN_HH
|
||||
# define SPOT_LTLVISIT_CONTAIN_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
||||
|
|
@ -81,5 +80,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_CONTAIN_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_DOTTY_HH
|
||||
# define SPOT_LTLVISIT_DOTTY_HH
|
||||
#pragma once
|
||||
|
||||
#include <ltlast/formula.hh>
|
||||
#include <iosfwd>
|
||||
|
|
@ -41,5 +40,3 @@ namespace spot
|
|||
std::ostream& dotty(std::ostream& os, const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_DOTTY_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_DUMP_HH
|
||||
# define SPOT_LTLVISIT_DUMP_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include <iosfwd>
|
||||
|
|
@ -40,5 +39,3 @@ namespace spot
|
|||
std::ostream& dump(std::ostream& os, const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_DUMP_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_LBT_HH
|
||||
# define SPOT_LTLVISIT_LBT_HH
|
||||
#pragma once
|
||||
|
||||
#include <ltlast/formula.hh>
|
||||
#include <iosfwd>
|
||||
|
|
@ -58,5 +57,3 @@ namespace spot
|
|||
/// @}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_TOSTRING_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_LENGTH_HH
|
||||
# define SPOT_LTLVISIT_LENGTH_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
|
||||
|
|
@ -53,5 +52,3 @@ namespace spot
|
|||
int length_boolone(const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_LENGTH_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_LUNABBREV_HH
|
||||
# define SPOT_LTLVISIT_LUNABBREV_HH
|
||||
#pragma once
|
||||
|
||||
#include "clone.hh"
|
||||
|
||||
|
|
@ -65,5 +64,3 @@ namespace spot
|
|||
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_LUNABBREV_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_MARK_HH
|
||||
# define SPOT_LTLVISIT_MARK_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "ltlast/visitor.hh"
|
||||
|
|
@ -53,5 +52,3 @@ namespace spot
|
|||
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_MARK_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_MUTATION_HH
|
||||
# define SPOT_LTLVISIT_MUTATION_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include <set>
|
||||
|
|
@ -48,4 +47,3 @@ namespace spot
|
|||
bool sort = true);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_NENOFORM_HH
|
||||
# define SPOT_LTLVISIT_NENOFORM_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
|
||||
|
|
@ -48,5 +47,3 @@ namespace spot
|
|||
negative_normal_form(const formula* f, bool negated = false);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_NENOFORM_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_POSTFIX_HH
|
||||
# define SPOT_LTLVISIT_POSTFIX_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "ltlast/visitor.hh"
|
||||
|
|
@ -59,5 +58,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_POSTFIX_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_RANDOMLTL_HH
|
||||
# define SPOT_LTLVISIT_RANDOMLTL_HH
|
||||
#pragma once
|
||||
|
||||
#include "apcollect.hh"
|
||||
#include <iosfwd>
|
||||
|
|
@ -354,4 +353,3 @@ namespace spot
|
|||
};
|
||||
}
|
||||
}
|
||||
#endif // SPOT_LTLVIST_RANDOMLTL_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_RELABEL_HH
|
||||
# define SPOT_LTLVISIT_RELABEL_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "misc/hash.hh"
|
||||
|
|
@ -60,10 +59,5 @@ namespace spot
|
|||
SPOT_API
|
||||
const formula* relabel_bse(const formula* f, relabeling_style style,
|
||||
relabeling_map* m = 0);
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
#endif // SPOT_LTLVISIT_RELABEL_HH
|
||||
|
|
|
|||
|
|
@ -17,10 +17,9 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_REMOVE_X_HH
|
||||
# define SPOT_LTLVISIT_REMOVE_X_HH
|
||||
#pragma once
|
||||
|
||||
# include "misc/common.hh"
|
||||
#include "misc/common.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -50,5 +49,3 @@ namespace spot
|
|||
const formula* remove_x(const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_ETESSAMI00_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_SIMPFG_HH
|
||||
# define SPOT_LTLVISIT_SIMPFG_HH
|
||||
#pragma once
|
||||
|
||||
#include "clone.hh"
|
||||
|
||||
|
|
@ -67,5 +66,3 @@ namespace spot
|
|||
SPOT_API const formula* simplify_f_g(const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_LUNABBREV_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_SIMPLIFY_HH
|
||||
# define SPOT_LTLVISIT_SIMPLIFY_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include <bddx.h>
|
||||
|
|
@ -202,7 +201,4 @@ namespace spot
|
|||
void operator=(const ltl_simplifier&) SPOT_DELETED;
|
||||
};
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_SIMPLIFY_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_SNF_HH
|
||||
#define SPOT_LTLVISIT_SNF_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "misc/hash.hh"
|
||||
|
|
@ -58,5 +57,3 @@ namespace spot
|
|||
star_normal_form_bounded(const formula* sere, snf_cache* cache = 0);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_SNF_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_TOSTRING_HH
|
||||
# define SPOT_LTLVISIT_TOSTRING_HH
|
||||
#pragma once
|
||||
|
||||
#include <ltlast/formula.hh>
|
||||
#include <iosfwd>
|
||||
|
|
@ -147,5 +146,3 @@ namespace spot
|
|||
/// @}
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_TOSTRING_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_TUNABBREV_HH
|
||||
# define SPOT_LTLVISIT_TUNABBREV_HH
|
||||
#pragma once
|
||||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
|
|
@ -68,5 +67,3 @@ namespace spot
|
|||
SPOT_API const formula* unabbreviate_ltl(const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_TUNABBREV_HH
|
||||
|
|
|
|||
|
|
@ -17,10 +17,9 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_LTLVISIT_WMUNABBREV_HH
|
||||
# define SPOT_LTLVISIT_WMUNABBREV_HH
|
||||
#pragma once
|
||||
|
||||
# include "misc/common.hh"
|
||||
#include "misc/common.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -40,5 +39,3 @@ namespace spot
|
|||
SPOT_API const formula* unabbreviate_wm(const formula* f);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_LTLVISIT_WMUNABBREV_HH
|
||||
|
|
|
|||
|
|
@ -20,11 +20,10 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_BAREWORD_HH
|
||||
# define SPOT_MISC_BAREWORD_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <string>
|
||||
#include "common.hh"
|
||||
#include <string>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -49,5 +48,3 @@ namespace spot
|
|||
SPOT_API bool is_spin_ap(const char* str);
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_BAREWORD_HH
|
||||
|
|
|
|||
|
|
@ -20,11 +20,10 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_BDDLT_HH
|
||||
# define SPOT_MISC_BDDLT_HH
|
||||
#pragma once
|
||||
|
||||
# include <bddx.h>
|
||||
# include <functional>
|
||||
#include <bddx.h>
|
||||
#include <functional>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -51,7 +50,4 @@ namespace spot
|
|||
return b.id();
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_BDDLT_HH
|
||||
|
|
|
|||
|
|
@ -17,16 +17,15 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_BITVECT_HH
|
||||
# define SPOT_MISC_BITVECT_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <cstddef>
|
||||
# include <cstdlib>
|
||||
# include <cassert>
|
||||
# include <iosfwd>
|
||||
# include <iostream>
|
||||
# include <algorithm>
|
||||
#include "common.hh"
|
||||
#include <cstddef>
|
||||
#include <cstdlib>
|
||||
#include <cassert>
|
||||
#include <iosfwd>
|
||||
#include <iostream>
|
||||
#include <algorithm>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -533,6 +532,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_MISC_BITVECT_HH
|
||||
|
|
|
|||
|
|
@ -17,9 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_CASTS_HH
|
||||
# define SPOT_MISC_CASTS_HH
|
||||
|
||||
#pragma once
|
||||
|
||||
// We usually write code like
|
||||
// subclass* i = down_cast<subclass*>(m);
|
||||
|
|
@ -35,5 +33,3 @@
|
|||
#else
|
||||
# define down_cast dynamic_cast
|
||||
#endif
|
||||
|
||||
#endif // SPOT_MISC_CASTS_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
#include <cstdlib>
|
||||
#include <stdexcept>
|
||||
|
||||
#ifndef SPOT_MISC_COMMON_HH
|
||||
# define SPOT_MISC_COMMON_HH
|
||||
#pragma once
|
||||
|
||||
#ifdef __GNUC__
|
||||
#define SPOT_LIKELY(expr) __builtin_expect(!!(expr), 1)
|
||||
|
|
@ -110,5 +109,3 @@
|
|||
// Useful when forwarding methods such as:
|
||||
// auto func(int param) SPOT_RETURN(implem_.func(param));
|
||||
#define SPOT_RETURN(code) -> decltype(code) { return code; }
|
||||
|
||||
#endif // SPOT_MISC_COMMON_HH
|
||||
|
|
|
|||
|
|
@ -20,12 +20,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_ESCAPE_HH
|
||||
# define SPOT_MISC_ESCAPE_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <iosfwd>
|
||||
# include <string>
|
||||
#include "common.hh"
|
||||
#include <iosfwd>
|
||||
#include <string>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -68,5 +67,3 @@ namespace spot
|
|||
trim(std::string& str);
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_ESCAPE_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_FIXPOOL_HH
|
||||
# define SPOT_MISC_FIXPOOL_HH
|
||||
#pragma once
|
||||
|
||||
#include <new>
|
||||
#include <cstddef>
|
||||
|
|
@ -109,7 +108,4 @@ namespace spot
|
|||
// chunk = several agglomerated blocks
|
||||
union chunk_ { chunk_* prev; char data_[1]; }* chunklist_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_FIXPOOL_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_FORMATER_HH
|
||||
#define SPOT_MISC_FORMATER_HH
|
||||
#pragma once
|
||||
|
||||
#include "common.hh"
|
||||
#include <iostream>
|
||||
|
|
@ -198,7 +197,4 @@ namespace spot
|
|||
protected:
|
||||
std::ostream* output_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_FORMATER_HH
|
||||
|
|
|
|||
|
|
@ -20,16 +20,15 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_HASH_HH
|
||||
# define SPOT_MISC_HASH_HH
|
||||
#pragma once
|
||||
|
||||
# include <string>
|
||||
# include <functional>
|
||||
# include "misc/hashfunc.hh"
|
||||
# include "misc/_config.h"
|
||||
#include <string>
|
||||
#include <functional>
|
||||
#include "misc/hashfunc.hh"
|
||||
#include "misc/_config.h"
|
||||
|
||||
# include <unordered_map>
|
||||
# include <unordered_set>
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -89,7 +88,4 @@ namespace spot
|
|||
static_cast<size_t>(uh(p.second)));
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_HASH_HH
|
||||
|
|
|
|||
|
|
@ -20,9 +20,9 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_HASHFUNC_HH
|
||||
# define SPOT_MISC_HASHFUNC_HH
|
||||
# include <cstddef>
|
||||
#pragma once
|
||||
|
||||
#include <cstddef>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -62,5 +62,3 @@ namespace spot
|
|||
}
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_HASHFUNC_HH
|
||||
|
|
|
|||
|
|
@ -17,12 +17,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_INTVCMP2_HH
|
||||
# define SPOT_MISC_INTVCMP2_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <vector>
|
||||
# include <stddef.h>
|
||||
#include "common.hh"
|
||||
#include <vector>
|
||||
#include <stddef.h>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -49,5 +48,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_INTVCMP2_HH
|
||||
|
|
|
|||
|
|
@ -17,12 +17,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_INTVCOMP_HH
|
||||
# define SPOT_MISC_INTVCOMP_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <vector>
|
||||
# include <stddef.h>
|
||||
#include "common.hh"
|
||||
#include <vector>
|
||||
#include <stddef.h>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -74,5 +73,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_INTVCOMP_HH
|
||||
|
|
|
|||
|
|
@ -33,10 +33,9 @@
|
|||
This special exception was added by the Free Software Foundation in
|
||||
version 2.2 of Bison. */
|
||||
|
||||
#ifndef SPOT_MISC_LOCATION_HH
|
||||
# define SPOT_MISC_LOCATION_HH
|
||||
#pragma once
|
||||
|
||||
# include "position.hh"
|
||||
#include "position.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -168,5 +167,3 @@ namespace spot
|
|||
return ostr;
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_LOCATION_HH
|
||||
|
|
|
|||
|
|
@ -20,11 +20,10 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_LTSTR_HH
|
||||
# define SPOT_MISC_LTSTR_HH
|
||||
#pragma once
|
||||
|
||||
# include <cstring>
|
||||
# include <functional>
|
||||
#include <cstring>
|
||||
#include <functional>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -50,5 +49,3 @@ namespace spot
|
|||
}
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_LTSTR_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_MEMUSAGE_HH
|
||||
# define SPOT_MISC_MEMUSAGE_HH
|
||||
#pragma once
|
||||
|
||||
#include "common.hh"
|
||||
|
||||
|
|
@ -33,5 +32,3 @@ namespace spot
|
|||
/// -1 otherwise.
|
||||
SPOT_API int memusage();
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_MEMUSAGE_HH
|
||||
|
|
|
|||
|
|
@ -20,12 +20,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_MINATO_HH
|
||||
# define SPOT_MISC_MINATO_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <bddx.h>
|
||||
# include <stack>
|
||||
#include "common.hh"
|
||||
#include <bddx.h>
|
||||
#include <stack>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -92,5 +91,3 @@ namespace spot
|
|||
bdd ret_;
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_MINATO_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_MSPOOL_HH
|
||||
# define SPOT_MISC_MSPOOL_HH
|
||||
#pragma once
|
||||
|
||||
#include <new>
|
||||
#include <cstddef>
|
||||
|
|
@ -124,7 +123,4 @@ namespace spot
|
|||
// chunk = several agglomerated blocks
|
||||
union chunk_ { chunk_* prev; char data_[1]; }* chunklist_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_INTVPOOL_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_OPTIONMAP_HH
|
||||
# define SPOT_MISC_OPTIONMAP_HH
|
||||
#pragma once
|
||||
|
||||
#include "common.hh"
|
||||
#include <string>
|
||||
|
|
@ -87,5 +86,3 @@ namespace spot
|
|||
std::map<std::string, int> options_;
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_OPTIONMAP_HH
|
||||
|
|
|
|||
|
|
@ -33,20 +33,19 @@
|
|||
This special exception was added by the Free Software Foundation in
|
||||
version 2.2 of Bison. */
|
||||
|
||||
#ifndef SPOT_MISC_POSITION_HH
|
||||
# define SPOT_MISC_POSITION_HH
|
||||
#pragma once
|
||||
|
||||
# include <algorithm> // std::max
|
||||
# include <iostream>
|
||||
# include <string>
|
||||
#include <algorithm> // std::max
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
|
||||
# ifndef YY_NULL
|
||||
# if defined __cplusplus && 201103L <= __cplusplus
|
||||
# define YY_NULL nullptr
|
||||
# else
|
||||
# define YY_NULL 0
|
||||
# endif
|
||||
#ifndef YY_NULL
|
||||
# if defined __cplusplus && 201103L <= __cplusplus
|
||||
# define YY_NULL nullptr
|
||||
# else
|
||||
# define YY_NULL 0
|
||||
# endif
|
||||
#endif
|
||||
|
||||
|
||||
namespace spot
|
||||
|
|
@ -162,8 +161,4 @@ namespace spot
|
|||
ostr << *pos.filename << ':';
|
||||
return ostr << pos.line << '.' << pos.column;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_POSITION_HH
|
||||
|
|
|
|||
|
|
@ -20,12 +20,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_RANDOM_HH
|
||||
# define SPOT_MISC_RANDOM_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <cmath>
|
||||
# include <vector>
|
||||
#include "common.hh"
|
||||
#include <cmath>
|
||||
#include <vector>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -137,5 +136,3 @@ namespace spot
|
|||
}
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_RANDOM_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_SATSOLVER_HH
|
||||
#define SPOT_MISC_SATSOLVER_HH
|
||||
#pragma once
|
||||
|
||||
#include "common.hh"
|
||||
#include "tmpfile.hh"
|
||||
|
|
@ -99,5 +98,3 @@ namespace spot
|
|||
SPOT_API satsolver::solution
|
||||
satsolver_get_solution(const char* filename);
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_SATSOLVER_HH
|
||||
|
|
|
|||
|
|
@ -20,20 +20,19 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_TIMER_HH
|
||||
# define SPOT_MISC_TIMER_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include "misc/_config.h"
|
||||
# include <cassert>
|
||||
# include <iosfwd>
|
||||
# include <string>
|
||||
# include <map>
|
||||
# include <chrono>
|
||||
# if SPOT_HAVE_SYS_TIMES_H
|
||||
# include <sys/times.h>
|
||||
# endif
|
||||
# include <ctime>
|
||||
#include "common.hh"
|
||||
#include "misc/_config.h"
|
||||
#include <cassert>
|
||||
#include <iosfwd>
|
||||
#include <string>
|
||||
#include <map>
|
||||
#include <chrono>
|
||||
#if SPOT_HAVE_SYS_TIMES_H
|
||||
# include <sys/times.h>
|
||||
#endif
|
||||
#include <ctime>
|
||||
|
||||
|
||||
namespace spot
|
||||
|
|
@ -247,5 +246,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_TIMER_HH
|
||||
|
|
|
|||
|
|
@ -17,15 +17,14 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_TMPFILE_HH
|
||||
# define SPOT_MISC_TMPFILE_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
# include <new>
|
||||
# include <stdexcept>
|
||||
# include <iostream>
|
||||
# include <list>
|
||||
# include "formater.hh"
|
||||
#include "common.hh"
|
||||
#include <new>
|
||||
#include <stdexcept>
|
||||
#include <iostream>
|
||||
#include <list>
|
||||
#include "formater.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -138,6 +137,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_MISC_TMPFILE_HH
|
||||
|
|
|
|||
|
|
@ -20,10 +20,9 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_MISC_VERSION_HH
|
||||
# define SPOT_MISC_VERSION_HH
|
||||
#pragma once
|
||||
|
||||
# include "common.hh"
|
||||
#include "common.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -31,5 +30,3 @@ namespace spot
|
|||
/// \brief Return Spot's version.
|
||||
SPOT_API const char* version();
|
||||
}
|
||||
|
||||
#endif // SPOT_MISC_VERSION_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_PRIV_ACCMAP_HH
|
||||
# define SPOT_PRIV_ACCMAP_HH
|
||||
#pragma once
|
||||
|
||||
#include <bddx.h>
|
||||
#include "misc/hash.hh"
|
||||
|
|
@ -118,5 +117,3 @@ namespace spot
|
|||
}
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_PRIV_ACCCONV_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_PRIV_BDDALLOC_HH
|
||||
# define SPOT_PRIV_BDDALLOC_HH
|
||||
#pragma once
|
||||
|
||||
#include "freelist.hh"
|
||||
#include <list>
|
||||
|
|
@ -52,7 +51,4 @@ namespace spot
|
|||
void extvarnum(int more);
|
||||
virtual int extend(int n);
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_PRIV_BDDALLOC_HH
|
||||
|
|
|
|||
|
|
@ -20,9 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#ifndef SPOT_PRIV_FREELIST_HH
|
||||
# define SPOT_PRIV_FREELIST_HH
|
||||
#pragma once
|
||||
|
||||
#include <list>
|
||||
#include <utility>
|
||||
|
|
@ -79,7 +77,4 @@ namespace spot
|
|||
/// Remove \a n consecutive entries from the list, starting at \a base.
|
||||
void remove(free_list_type::iterator i, int base, int n);
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_PRIV_FREELIST_HH
|
||||
|
|
|
|||
|
|
@ -34,14 +34,13 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \
|
|||
-o -name "${1-*}.hxx" \) \
|
||||
-a -type f -a -print | sed "s,$INCDIR/,,g"`; do
|
||||
|
||||
b=`echo "$file" | tr '[/.a-z]' '[__A-Z]'`
|
||||
if grep "[ ]*#.*def.* SPOT_$b\$" "$INCDIR/$file" >/dev/null; then
|
||||
if head -n 100 "$INCDIR/$file" | grep -q "[ ]*#.*pragma.* once\$"; then
|
||||
:
|
||||
elif grep 'GNU Bison 2\.6' "$INCDIR/$file" >/dev/null; then
|
||||
elif grep -q 'GNU Bison 2\.6' "$INCDIR/$file"; then
|
||||
# Bison 2.6, 2.6.1, 2.6.2 have a bug where position.hh
|
||||
# include <iosfwd> instead of <iostream>.
|
||||
continue
|
||||
elif grep 'GNU Bison' "$INCDIR/$file" >/dev/null; then
|
||||
elif grep -q 'GNU Bison' "$INCDIR/$file"; then
|
||||
:
|
||||
else
|
||||
echo "Missing, or incorrect include guard." >&2
|
||||
|
|
@ -49,24 +48,7 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \
|
|||
echo " $file" >> failures
|
||||
continue
|
||||
fi
|
||||
|
||||
cat >incltest.cc <<EOF
|
||||
// Include the file twice, so we detect missing inclusion guards.
|
||||
#include <$file>
|
||||
#include <$file>
|
||||
EOF
|
||||
|
||||
case $file in
|
||||
*bin/*) MOREFLAGS="-I $TOPBUILD/lib/ -I $INCDIR/../lib/ -I $TOPBUILD";;
|
||||
*) MOREFLAGS=;;
|
||||
esac
|
||||
|
||||
if $CXX $MOREFLAGS $CPPFLAGS -DSKIP_DEPRECATED_WARNING $CXXFLAGS -c incltest.cc; then
|
||||
echo "PASS: $file"
|
||||
else
|
||||
echo "FAIL: $file"
|
||||
echo " $file" >> failures
|
||||
fi
|
||||
echo "PASS: $file"
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TA_HH
|
||||
# define SPOT_TA_TA_HH
|
||||
#pragma once
|
||||
|
||||
#include <set>
|
||||
|
||||
|
|
@ -296,8 +295,4 @@ namespace spot
|
|||
|
||||
/// \addtogroup ta_misc Miscellaneous algorithms on TA
|
||||
/// \ingroup ta_algorithms
|
||||
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TA_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TAEXPLICIT_HH
|
||||
# define SPOT_TA_TAEXPLICIT_HH
|
||||
#pragma once
|
||||
|
||||
#include "misc/hash.hh"
|
||||
#include <list>
|
||||
|
|
@ -260,7 +259,4 @@ namespace spot
|
|||
{
|
||||
return std::make_shared<ta_explicit>(tgba, n_acc, artificial_initial_state);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TAEXPLICIT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TAPRODUCT_HH
|
||||
# define SPOT_TA_TAPRODUCT_HH
|
||||
#pragma once
|
||||
|
||||
#include "ta.hh"
|
||||
#include "kripke/kripke.hh"
|
||||
|
|
@ -219,7 +218,4 @@ namespace spot
|
|||
/// \brief Move to the next successor in the Kripke structure
|
||||
void next_kripke_dest();
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TAPRODUCT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TGTA_HH
|
||||
# define SPOT_TA_TGTA_HH
|
||||
#pragma once
|
||||
|
||||
#include "tgba/tgba.hh"
|
||||
|
||||
|
|
@ -57,7 +56,6 @@ namespace spot
|
|||
/// obtained by querying the iterator over the successors of
|
||||
/// a state.
|
||||
|
||||
|
||||
class SPOT_API tgta : public tgba
|
||||
{
|
||||
|
||||
|
|
@ -83,5 +81,3 @@ namespace spot
|
|||
typedef std::shared_ptr<tgta> tgta_ptr;
|
||||
typedef std::shared_ptr<const tgta> const_tgta_ptr;
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TGTA_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TGTAEXPLICIT_HH
|
||||
# define SPOT_TA_TGTAEXPLICIT_HH
|
||||
#pragma once
|
||||
|
||||
#include "misc/hash.hh"
|
||||
#include <list>
|
||||
|
|
@ -76,5 +75,3 @@ namespace spot
|
|||
artificial_initial_state);
|
||||
}
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TGTAEXPLICIT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TA_TGTAPRODUCT_HH
|
||||
# define SPOT_TA_TGTAPRODUCT_HH
|
||||
#pragma once
|
||||
|
||||
#include "tgba/tgba.hh"
|
||||
#include "tgba/tgbaproduct.hh"
|
||||
|
|
@ -100,7 +99,4 @@ namespace spot
|
|||
bdd kripke_source_condition;
|
||||
state* kripke_current_dest_state;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TA_TGTAPRODUCT_HH
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TAALGOS_DOTTY_HH
|
||||
# define SPOT_TAALGOS_DOTTY_HH
|
||||
#pragma once
|
||||
|
||||
#include "ta/ta.hh"
|
||||
#include <iosfwd>
|
||||
|
|
@ -28,5 +27,3 @@ namespace spot
|
|||
SPOT_API std::ostream&
|
||||
dotty_reachable(std::ostream& os, const const_ta_ptr& a);
|
||||
}
|
||||
|
||||
#endif // SPOT_TAALGOS_DOTTY_HH
|
||||
|
|
|
|||
|
|
@ -20,8 +20,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TAALGOS_EMPTINESSTA_HH
|
||||
# define SPOT_TAALGOS_EMPTINESSTA_HH
|
||||
#pragma once
|
||||
|
||||
#include "ta/taproduct.hh"
|
||||
#include "misc/optionmap.hh"
|
||||
|
|
@ -160,5 +159,3 @@ namespace spot
|
|||
/// \addtogroup ta_emptiness_check_algorithms Emptiness-check algorithms
|
||||
/// \ingroup ta_emptiness_check
|
||||
}
|
||||
|
||||
#endif // SPOT_TAALGOS_EMPTINESSTA_HH
|
||||
|
|
|
|||
|
|
@ -17,12 +17,11 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TAALGOS_MINIMIZE_HH
|
||||
# define SPOT_TAALGOS_MINIMIZE_HH
|
||||
#pragma once
|
||||
|
||||
# include "ta/ta.hh"
|
||||
# include "ta/tgta.hh"
|
||||
# include "ta/tgtaexplicit.hh"
|
||||
#include "ta/ta.hh"
|
||||
#include "ta/tgta.hh"
|
||||
#include "ta/tgtaexplicit.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -75,5 +74,3 @@ namespace spot
|
|||
|
||||
/// @}
|
||||
}
|
||||
|
||||
#endif /* !SPOT_TAALGOS_MINIMIZE_HH */
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@
|
|||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_TAALGOS_REACHITER_HH
|
||||
# define SPOT_TAALGOS_REACHITER_HH
|
||||
#pragma once
|
||||
|
||||
#include "misc/hash.hh"
|
||||
#include "ta/ta.hh"
|
||||
|
|
@ -129,7 +128,4 @@ namespace spot
|
|||
protected:
|
||||
std::deque<const state*> todo; ///< A queue of states yet to explore.
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TAALGOS_REACHITER_HH
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Add a link
Reference in a new issue