environment.hh 1.29 KB
Newer Older
 Alexandre Duret-Lutz committed Apr 17, 2003 1 2 3 ``````#ifndef SPOT_LTLENV_ENVIRONMENT_HH # define SPOT_LTLENV_ENVIRONMENT_HH `````` Alexandre Duret-Lutz committed Apr 17, 2003 4 ``````# include "ltlast/formula.hh" `````` Alexandre Duret-Lutz committed Apr 17, 2003 5 6 7 8 9 10 11 ``````# include namespace spot { namespace ltl { `````` Alexandre Duret-Lutz committed Apr 18, 2003 12 `````` /// An environment that describe atomic propositions. `````` Alexandre Duret-Lutz committed Apr 17, 2003 13 14 15 `````` class environment { public: `````` Alexandre Duret-Lutz committed Apr 18, 2003 16 17 18 `````` /// \brief Obtain the formula associated to \a prop_str /// /// Usually \a prop_str, is the name of an atomic proposition, `````` Alexandre Duret-Lutz committed Jun 05, 2003 19 `````` /// a spot::ltl::require simply returns the associated `````` Alexandre Duret-Lutz committed Apr 18, 2003 20 21 22 23 24 `````` /// spot::ltl::atomic_prop. /// /// Note this is not a \c const method. Some environment will /// "create" the atomic proposition when asked. /// `````` Alexandre Duret-Lutz committed Jun 05, 2003 25 `````` /// We return a spot::ltl::formula instead of an `````` Alexandre Duret-Lutz committed Apr 18, 2003 26 27 28 29 30 31 32 `````` /// spot::ltl::atomic_prop, because this /// will allow nifty tricks (e.g., we could name formulae in an /// environment, and let the parser build a larger tree from /// these). /// /// \return 0 iff \a prop_str is not part of the environment, /// or the associated spot::ltl::formula otherwise. `````` Alexandre Duret-Lutz committed Jun 05, 2003 33 `````` virtual formula* require(const std::string& prop_str) = 0; `````` Alexandre Duret-Lutz committed Apr 17, 2003 34 `````` `````` Alexandre Duret-Lutz committed Apr 18, 2003 35 `````` /// Get the name of the environment. `````` Alexandre Duret-Lutz committed Apr 17, 2003 36 `````` virtual const std::string& name() = 0; `````` Alexandre Duret-Lutz committed Apr 18, 2003 37 `````` `````` Alexandre Duret-Lutz committed Apr 17, 2003 38 39 40 41 42 43 44 45 `````` // FIXME: More functions will be needed later, but // it's enough for now. }; } } #endif // SPOT_LTLENV_ENVIRONMENT_HH``````