Awali
Another Weighted Automata library
zmax.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2022 Sylvain Lombardy, Victor Marsault, Jacques Sakarovitch
3 //
4 // Awali is a free software: you can redistribute it and/or modify
5 // it under the terms of the GNU General Public License as published by
6 // the Free Software Foundation, either version 3 of the License, or
7 // (at your option) any later version.
8 //
9 // This program is distributed in the hope that it will be useful,
10 // but WITHOUT ANY WARRANTY; without even the implied warranty of
11 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 // GNU General Public License for more details.
13 //
14 // You should have received a copy of the GNU General Public License
15 // along with this program. If not, see <http://www.gnu.org/licenses/>.
16 
17 #ifndef AWALI_WEIGHTSET_ZMAX_HH
18 # define AWALI_WEIGHTSET_ZMAX_HH
19 
20 # include <limits>
21 # include <ostream>
22 # include <string>
23 # include <sstream>
24 # include <utility>
25 
26 #include <awali/sttc/misc/raise.hh>
27 #include <awali/common/enums.hh>
28 #include <awali/sttc/misc/stream.hh> // eat
32 
33 namespace awali {
34  namespace sttc {
40  class zmax
41  {
42  public:
43  using self_type = zmax;
44 
45  static std::string sname()
46  {
47  return "zmax";
48  }
49 
50  std::string vname(bool = true) const
51  {
52  return sname();
53  }
54 
56  static zmax make(std::istream& is)
57  {
58  eat(is, sname());
59  return {};
60  }
61 
62  using value_t = int;
63 
64  static value_t
65  add(const value_t l, const value_t r)
66  {
67  return std::max(l, r);
68  }
69 
70  static value_t
71  mul(const value_t l, const value_t r)
72  {
73  return (is_zero(l) || is_zero(r) ? zero()
74  : l + r);
75  }
76 
77  static value_t
78  rdiv(const value_t l, const value_t r)
79  {
80  require(!is_zero(r), "div: division by zero");
81  return l - r;
82  }
83 
84  static value_t
85  ldiv(const value_t l, const value_t r)
86  {
87  return rdiv(r, l);
88  }
89 
90  value_t
91  star(const value_t v) const
92  {
93  if (0 >= v)
94  return one();
95  else
96  raise(sname(), ": star: invalid value: ", format(*this, v));
97  }
98 
99  static value_t
100  one()
101  {
102  return 0;
103  }
104 
105  static value_t
107  {
109  }
110 
111  static bool
112  equals(const value_t l, const value_t r)
113  {
114  return l == r;
115  }
116 
118  static bool less_than(value_t lhs, value_t rhs)
119  {
120  return lhs < rhs;
121  }
122 
123  constexpr static bool is_special(value_t)
124  {
125  return false;
126  }
127 
128  static bool
129  is_zero(const value_t v)
130  {
131  return v == zero();
132  }
133 
134  static bool
135  is_one(const value_t v)
136  {
137  return v == one();
138  }
139 
140  static constexpr bool is_commutative_semiring() { return true; }
141 
142  static constexpr bool show_one() { return true; }
143  static constexpr star_status_t star_status() { return star_status_t::TOPS; }
144 
145  static value_t
147  {
148  return v;
149  }
150 
151  static size_t hash(value_t v)
152  {
153  return utils::hash_value(v);
154  }
155 
156  static value_t
158  {
159  return v;
160  }
161 
162  static value_t
164  {
165  return v ? one() : zero();
166  }
167 
168  static value_t
169  conv(std::istream& stream)
170  {
171  int sign = 1;
172  switch (int i = stream.peek())
173  {
174  case '-':
175  stream.ignore();
176  if ( stream.peek() == 'o' ) {
177  stream.ignore();
178  if ( stream.get() == 'o')
179  return zero();
180  else
181  throw std::domain_error(sname() + ": invalid value: -o" + str_escape(i));
182  }
183  default:
184  if (stream >> i)
185  return i*sign;
186  else
187  sttc::fail_reading(stream, sname() + ": invalid value");
188  }
189  }
190 
191  static value_t
192  parse(const std::string & s, size_t& p) {
193  if (p>=3 && s[p-3]=='-' && s[p-2]=='o' && s[p-1]=='o'){
194  p -= 3;
195  return zero();
196  }
197  size_t i=p;
198  for(; i>0 && s[i-1]>='0' && s[i-1]<='9'; --i)
199  ;
200  if(i==p)
201  throw parse_exception("Wrong Z-max value");
202  if(i>0 && (s[i-1]=='-' || s[i-1]=='+'))
203  --i;
204  std::istringstream st(s.substr(i, p-i));
205  value_t x;
206  st >> x;
207  p=i;
208  return x;
209  }
210 
211  static std::ostream&
212  print(const value_t v, std::ostream& o,
213  const std::string& format = "text")
214  {
215  if(format == "json") {
216  if (is_zero(v))
217  o << "\"-oo\"";
218  else
219  o<< v;
220  return o;
221  }
222  if (is_zero(v))
223  o << (format == "latex" ? "-\\infty" : "-oo");
224  else
225  o << v;
226  return o;
227  }
228 
229  std::ostream&
230  print_set(std::ostream& o, const std::string& format = "text") const
231  {
232  if (format == "latex")
233  o << "\\mathbb{Z}_{max}";
234  else if (format == "text")
235  o << "Z-max-plus";
236  else
237  raise("invalid format: ", format);
238  return o;
239  }
240 
241  template<unsigned version = version::fsm_json>
242  value_t
243  static value_from_json(json::node_t const* p)
244  {
245  version::check_fsmjson<version>();
246  switch (version) {
247  case 0: /* Never occurs due to above check. */
248  case 1:
249  default:
250  try {
251  return p->to_int();
252  } catch (json::coercion_exception&) {}
253  try {
254  if (p->to_string() == "-oo")
255  return zero();
256  } catch (json::coercion_exception&) {}
257  std::stringstream ss;
258  ss << "[zmax] At position " << p->path_to_root()
259  << " node cannot be coerced to a Z-max-plus value.";
260  throw json::coercion_exception(ss.str());
261  }
262  }
263 
264  template<unsigned version = version::fsm_json>
265  json::node_t*
267  {
268  switch (version) {
269  case 0:
270  throw parse_exception("[zmax] Unsupported fsm-json version:"
271  + std::to_string(version));
272  case 1:
273  default:
274  if (v == zero())
275  return new json::string_t("-oo");
276  return new json::int_t(v);
277  }
278  }
279 
280  template<unsigned version = version::fsm_json>
281  json::node_t*
282  to_json() const
283  {
284  switch (version) {
285  case 0:
286  throw parse_exception("[zmin] Unsupported fsm-json version:"
287  + std::to_string(version));
288  case 1:
289  default:
290  return new json::object_t("semiring",new json::string_t("Z-max-plus"));
291  }
292  }
293 
294 
295  };
296 
297  inline zmax join(const zmax&, const zmax&) { return {}; }
298 
299  inline zmax join(const b&, const zmax&) { return {}; }
300  inline zmax join(const zmax&, const b&) { return {}; }
301 
302 }}//end of ns awali::stc
303 
304 #endif // !AWALI_WEIGHTSET_ZMAX_HH
Exception used when trying to coerce a node to a given type.
Definition: node.hh:143
Definition: node.hh:488
Definition: node.hh:193
path_t path_to_root() const
virtual std::string to_string() const
Coerces this node_t to an std::string.
Definition: node.hh:331
virtual int to_int() const
Coerces this node_t to int.
Definition: node.hh:321
Definition: node.hh:367
Definition: node.hh:529
The Boolean semring.
Definition: b.hh:38
bool value_t
Definition: b.hh:56
The semiring of floating Numbers.
Definition: r.hh:35
The Z-max-plus semiring.
Definition: zmax.hh:41
std::ostream & print_set(std::ostream &o, const std::string &format="text") const
Definition: zmax.hh:230
static value_t zero()
Definition: zmax.hh:106
static value_t one()
Definition: zmax.hh:100
static value_t conv(std::istream &stream)
Definition: zmax.hh:169
static value_t conv(self_type, value_t v)
Definition: zmax.hh:157
json::node_t * value_to_json(value_t v) const
Definition: zmax.hh:266
static value_t parse(const std::string &s, size_t &p)
Definition: zmax.hh:192
constexpr static bool is_special(value_t)
Definition: zmax.hh:123
static bool is_one(const value_t v)
Definition: zmax.hh:135
std::string vname(bool=true) const
Definition: zmax.hh:50
static zmax make(std::istream &is)
Build from the description in is.
Definition: zmax.hh:56
int value_t
Definition: zmax.hh:62
static value_t conv(b, b::value_t v)
Definition: zmax.hh:163
static std::string sname()
Definition: zmax.hh:45
static constexpr bool show_one()
Definition: zmax.hh:142
static std::ostream & print(const value_t v, std::ostream &o, const std::string &format="text")
Definition: zmax.hh:212
value_t star(const value_t v) const
Definition: zmax.hh:91
static value_t rdiv(const value_t l, const value_t r)
Definition: zmax.hh:78
static value_t transpose(const value_t v)
Definition: zmax.hh:146
static constexpr bool is_commutative_semiring()
Definition: zmax.hh:140
static value_t add(const value_t l, const value_t r)
Definition: zmax.hh:65
static size_t hash(value_t v)
Definition: zmax.hh:151
static bool equals(const value_t l, const value_t r)
Definition: zmax.hh:112
static constexpr star_status_t star_status()
Definition: zmax.hh:143
static bool is_zero(const value_t v)
Definition: zmax.hh:129
static value_t mul(const value_t l, const value_t r)
Definition: zmax.hh:71
json::node_t * to_json() const
Definition: zmax.hh:282
static bool less_than(value_t lhs, value_t rhs)
Whether lhs < rhs.
Definition: zmax.hh:118
static value_t ldiv(const value_t l, const value_t r)
Definition: zmax.hh:85
static value_t value_from_json(json::node_t const *p)
Definition: zmax.hh:243
star_status_t
The different behaviours a weightset may have with respect to the star.
Definition: enums.hh:163
@ TOPS
Definition: enums.hh:167
std::string to_string(identities i)
void eat(std::istream &is, char c)
Check lookahead character and advance.
Definition: stream.hh:62
ATTRIBUTE_NORETURN void fail_reading(std::istream &is, std::string explanation)
Throw an exception after failing to read from is.
Definition: stream.hh:93
auto join(const ratexpset< Ctx1 > &a, const ratexpset< Ctx2 > &b) -> ratexpset< join_t< Ctx1, Ctx2 >>
The union of two ratexpsets.
Definition: ratexpset.hh:445
std::ostream & str_escape(std::ostream &os, const int c)
Definition: escape.hh:30
auto format(const ValueSet &vs, const typename ValueSet::value_t &v, Args &&... args) -> std::string
Format v via vs.print.
Definition: stream.hh:109
void require(bool b, Args &&... args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:55
std::size_t hash_value(const T &v)
Definition: hash.hh:76
ATTRIBUTE_CONST int max(int a, int b)
Definition: arith.hh:54
ATTRIBUTE_CONST int min(int a, int b)
Definition: arith.hh:48
Main namespace of Awali.
Definition: ato.hh:22
Exceptions thrown during parsing.
Definition: parse_exception.hh:26