environment.hh 1.29 KB
Newer Older
1
2
3
#ifndef SPOT_LTLENV_ENVIRONMENT_HH
# define SPOT_LTLENV_ENVIRONMENT_HH

4
# include "ltlast/formula.hh"
5
6
7
8
9
10
11
# include <string>

namespace spot
{
  namespace ltl
  {

12
    /// An environment that describe atomic propositions.
13
14
15
    class environment
    {
    public:
16
17
18
      /// \brief Obtain the formula associated to \a prop_str
      ///
      /// Usually \a prop_str, is the name of an atomic proposition,
19
      /// a spot::ltl::require simply returns the associated
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.
      ///
25
      /// We return a spot::ltl::formula instead of an
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.
33
      virtual formula* require(const std::string& prop_str) = 0;
34

35
      /// Get the name of the environment.
36
      virtual const std::string& name() = 0;
37

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