Awali
Another Weighted Automata library
zmin.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2023 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_ZMIN_HH
18 # define AWALI_WEIGHTSET_ZMIN_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 {
35 
41  class zmin
42  {
43  public:
44  using self_type = zmin;
45 
46  static std::string sname()
47  {
48  return "zmin";
49  }
50 
51  std::string vname(bool = true) const
52  {
53  return sname();
54  }
55 
57  static zmin make(std::istream& is)
58  {
59  eat(is, sname());
60  return {};
61  }
62 
63  using value_t = int;
64 
65  static value_t
66  add(const value_t l, const value_t r)
67  {
68  return std::min(l, r);
69  }
70 
71  static value_t
72  mul(const value_t l, const value_t r)
73  {
74  return (is_zero(l) || is_zero(r) ? zero()
75  : l + r);
76  }
77 
78  static value_t
79  rdiv(const value_t l, const value_t r)
80  {
81  require(!is_zero(r), "div: division by zero");
82  return l - r;
83  }
84 
85  static value_t
86  ldiv(const value_t l, const value_t r)
87  {
88  return rdiv(r, l);
89  }
90 
91  value_t
92  star(const value_t v) const
93  {
94  if (0 <= v)
95  return one();
96  else
97  raise(sname(), ": star: invalid value: ", format(*this, v));
98  }
99 
100  value_t
101  plus(const value_t v) const
102  {
103  if (0 <= v)
104  return v;
105  else
106  raise(sname(), ": star: invalid value: ", format(*this, v));
107  }
108 
109  static value_t
110  one()
111  {
112  return 0;
113  }
114 
115  static value_t
117  {
119  }
120 
121  static bool
122  equals(const value_t l, const value_t r)
123  {
124  return l == r;
125  }
126 
128  static bool less_than(value_t lhs, value_t rhs)
129  {
130  return lhs > rhs;
131  }
132 
133  constexpr static bool is_special(value_t)
134  {
135  return false;
136  }
137 
138  static bool
139  is_zero(const value_t v)
140  {
141  return v == zero();
142  }
143 
144  static bool
145  is_one(const value_t v)
146  {
147  return v == one();
148  }
149 
150  static constexpr bool is_commutative_semiring() { return true; }
151 
152  static constexpr bool show_one() { return true; }
153  static constexpr star_status_t star_status() { return star_status_t::TOPS; }
154 
155  static value_t
157  {
158  return v;
159  }
160 
161  static size_t hash(value_t v)
162  {
163  return utils::hash_value(v);
164  }
165 
166  static value_t
168  {
169  return v;
170  }
171 
172  static value_t
174  {
175  return v ? one() : zero();
176  }
177 
178  static value_t
179  conv(std::istream& stream)
180  {
181  switch (int i = stream.peek())
182  {
183  case 'o':
184  stream.ignore();
185  if ((i = stream.get()) == 'o')
186  return zero();
187  else
188  throw std::domain_error(sname() + ": invalid value: o" + str_escape(i));
189  default:
190  if (stream >> i)
191  return i;
192  else
193  sttc::fail_reading(stream, sname() + ": invalid value");
194  }
195  }
196 
197  static value_t
198  parse(const std::string & s, size_t& p) {
199  if(p>=2 && s[p-2]=='o' && s[p-1]=='o'){
200  p -= 2;
201  return zero();
202  }
203  size_t i=p;
204  for(; i>0 && s[i-1]>='0' && s[i-1]<='9'; --i)
205  ;
206  if(i==p)
207  throw parse_exception("Wrong Z-min value");
208  if(i>0 && (s[i-1]=='-' || s[i-1]=='+'))
209  --i;
210  std::istringstream st(s.substr(i, p-i));
211  value_t x;
212  st >> x;
213  p=i;
214  return x;
215  }
216 
217  static std::ostream&
218  print(const value_t v, std::ostream& o,
219  const std::string& format = "text")
220  {
221  if(format == "json") {
222  if (is_zero(v))
223  o << "\"oo\"";
224  else
225  o<< v;
226  return o;
227  }
228  if (is_zero(v))
229  o << (format == "latex" ? "\\infty" : "oo");
230  else
231  o << v;
232  return o;
233  }
234 
235  std::ostream&
236  print_set(std::ostream& o, const std::string& format = "text") const
237  {
238  if (format == "latex")
239  o << "\\mathbb{Z}_{min}";
240  else if (format == "text")
241  o << "Z-min-plus";
242  else
243  raise("invalid format: ", format);
244  return o;
245  }
246 
247 
248  template<unsigned version = version::fsm_json>
249  value_t
250  static value_from_json(json::node_t const* p)
251  {
252  version::check_fsmjson<version>();
253  switch (version) {
254  case 0: /* Never occurs due to above check. */
255  case 1:
256  default:
257  try {
258  return p->to_int();
259  } catch (json::coercion_exception&) {}
260  try {
261  if (p->to_string() == "oo")
262  return zero();
263  } catch (json::coercion_exception&) {}
264  std::stringstream ss;
265  ss << "[zmin] At position " << p->path_to_root()
266  << " node cannot be coerced to a Z-min-plus value.";
267  throw json::coercion_exception(ss.str());
268  }
269  }
270 
271  template<unsigned version = version::fsm_json>
272  json::node_t*
274  {
275  version::check_fsmjson<version>();
276  switch (version) {
277  case 0: /* Never occurs due to above check. */
278  case 1:
279  default:
280  if (v == zero())
281  return new json::string_t("oo");
282  return new json::int_t(v);
283  }
284  }
285 
286  template<unsigned version = version::fsm_json>
287  json::node_t*
288  to_json() const
289  {
290  version::check_fsmjson<version>();
291  switch (version) {
292  case 0: /* Never occurs due to above check. */
293  case 1:
294  default:
295  return new json::object_t("semiring",new json::string_t("Z-min-plus"));
296  }
297  }
298 
299  };
300 
301  inline zmin join(const zmin&, const zmin&) { return {}; }
302 
303  inline zmin join(const b&, const zmin&) { return {}; }
304  inline zmin join(const zmin&, const b&) { return {}; }
305 
306  }}//end of ns awali::stc
307 
308 #endif // !AWALI_WEIGHTSET_ZMIN_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-min-plus semiring.
Definition: zmin.hh:42
static value_t mul(const value_t l, const value_t r)
Definition: zmin.hh:72
static zmin make(std::istream &is)
Build from the description in is.
Definition: zmin.hh:57
static constexpr bool show_one()
Definition: zmin.hh:152
static value_t rdiv(const value_t l, const value_t r)
Definition: zmin.hh:79
static std::string sname()
Definition: zmin.hh:46
static size_t hash(value_t v)
Definition: zmin.hh:161
json::node_t * to_json() const
Definition: zmin.hh:288
static value_t zero()
Definition: zmin.hh:116
static value_t add(const value_t l, const value_t r)
Definition: zmin.hh:66
static constexpr bool is_commutative_semiring()
Definition: zmin.hh:150
static constexpr star_status_t star_status()
Definition: zmin.hh:153
constexpr static bool is_special(value_t)
Definition: zmin.hh:133
std::string vname(bool=true) const
Definition: zmin.hh:51
static value_t ldiv(const value_t l, const value_t r)
Definition: zmin.hh:86
value_t plus(const value_t v) const
Definition: zmin.hh:101
static bool is_one(const value_t v)
Definition: zmin.hh:145
static value_t one()
Definition: zmin.hh:110
static value_t conv(self_type, value_t v)
Definition: zmin.hh:167
json::node_t * value_to_json(value_t v) const
Definition: zmin.hh:273
static value_t conv(b, b::value_t v)
Definition: zmin.hh:173
static value_t value_from_json(json::node_t const *p)
Definition: zmin.hh:250
std::ostream & print_set(std::ostream &o, const std::string &format="text") const
Definition: zmin.hh:236
static bool is_zero(const value_t v)
Definition: zmin.hh:139
static value_t transpose(const value_t v)
Definition: zmin.hh:156
static value_t conv(std::istream &stream)
Definition: zmin.hh:179
static bool less_than(value_t lhs, value_t rhs)
Whether lhs < rhs.
Definition: zmin.hh:128
static bool equals(const value_t l, const value_t r)
Definition: zmin.hh:122
value_t star(const value_t v) const
Definition: zmin.hh:92
int value_t
Definition: zmin.hh:63
static std::ostream & print(const value_t v, std::ostream &o, const std::string &format="text")
Definition: zmin.hh:218
static value_t parse(const std::string &s, size_t &p)
Definition: zmin.hh:198
star_status_t
The different behaviours a weightset may have with respect to the star.
Definition: enums.hh:163
@ TOPS
Definition: enums.hh:167
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:449
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