environment.hh 893 Bytes
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
12
13
14
15
16
17
18
# include <string>

namespace spot
{
  namespace ltl
  {

    class environment
    {
    public:
      // Check whether the environment contains the atomic proposition
      // described by prop_str.
      // Note this is NOT a const method.  Some environment will
      // "create" the atomic proposition when asked.
19
20
21
22
23
      // We return a formula instead of an 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).
      virtual formula* require(const std::string& prop_str) = 0; 
24
25
26
27
28
29
30
31
32
33

      virtual const std::string& name() = 0;
      // FIXME: More functions will be needed later, but
      // it's enough for now.
    };

  }
}

#endif // SPOT_LTLENV_ENVIRONMENT_HH