Awali
Another Weighted Automata library
zmax.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2021 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  switch (version) {
246  case 0: /* stored as string */
247  if (p->kind == json::STRING && p->to_string() == "oo")
248  return zero();
249  case 1:
250  default:
251  try {
252  return p->to_int();
253  } catch (json::coercion_exception&) {}
254  try {
255  if (p->to_string() == "-oo")
256  return zero();
257  } catch (json::coercion_exception&) {}
258  std::stringstream ss;
259  ss << "[zmax] At position " << p->path_to_root()
260  << " node cannot be coerced to a Z-max-plus value.";
261  throw json::coercion_exception(ss.str());
262  }
263  }
264 
265  template<unsigned version = version::fsm_json>
266  json::node_t*
268  {
269  switch (version) {
270  case 0:
271  throw parse_exception("[zmax] Unsupported fsm-json version:"
272  + std::to_string(version));
273  case 1:
274  default:
275  if (v == zero())
276  return new json::string_t("-oo");
277  return new json::int_t(v);
278  }
279  }
280 
281  template<unsigned version = version::fsm_json>
282  json::node_t*
283  to_json() const
284  {
285  switch (version) {
286  case 0:
287  throw parse_exception("[zmin] Unsupported fsm-json version:"
288  + std::to_string(version));
289  case 1:
290  default:
291  return new json::object_t("semiring",new json::string_t("Z-max-plus"));
292  }
293  }
294 
295 
296  };
297 
298  inline zmax join(const zmax&, const zmax&) { return {}; }
299 
300  inline zmax join(const b&, const zmax&) { return {}; }
301  inline zmax join(const zmax&, const b&) { return {}; }
302 
303 }}//end of ns awali::stc
304 
305 #endif // !AWALI_WEIGHTSET_ZMAX_HH
awali::sttc::zmax::is_zero
static bool is_zero(const value_t v)
Definition: zmax.hh:129
awali::sttc::b::value_t
bool value_t
Definition: b.hh:56
awali::sttc::zmax::less_than
static bool less_than(value_t lhs, value_t rhs)
Whether lhs < rhs.
Definition: zmax.hh:118
awali::sttc::zmax::mul
static value_t mul(const value_t l, const value_t r)
Definition: zmax.hh:71
awali
Main namespace of Awali.
Definition: ato.hh:22
awali::json::STRING
@ STRING
Definition: node.hh:94
awali::sttc::zmax::add
static value_t add(const value_t l, const value_t r)
Definition: zmax.hh:65
awali::sttc::zmax::ldiv
static value_t ldiv(const value_t l, const value_t r)
Definition: zmax.hh:85
awali::star_status_t
star_status_t
The different behaviours a weightset may have with respect to the star.
Definition: enums.hh:161
awali::sttc::zmax::value_t
int value_t
Definition: zmax.hh:62
awali::sttc::zmax::show_one
static constexpr bool show_one()
Definition: zmax.hh:142
awali::sttc::zmax::one
static value_t one()
Definition: zmax.hh:100
awali::sttc::join
auto join(const ratexpset< Ctx1 > &a, const ratexpset< Ctx2 > &b) -> ratexpset< join_t< Ctx1, Ctx2 >>
The union of two ratexpsets.
Definition: ratexpset.hh:448
awali::sttc::zmax::zero
static value_t zero()
Definition: zmax.hh:106
awali::sttc::zmax::conv
static value_t conv(self_type, value_t v)
Definition: zmax.hh:157
awali::utils::min
ATTRIBUTE_CONST int min(int a, int b)
Definition: arith.hh:48
awali::sttc::zmax::to_json
json::node_t * to_json() const
Definition: zmax.hh:283
awali::sttc::zmax::vname
std::string vname(bool=true) const
Definition: zmax.hh:50
awali::json::node_t::kind
const node_kind_t kind
Definition: node.hh:194
awali::sttc::zmax::hash
static size_t hash(value_t v)
Definition: zmax.hh:151
awali::sttc::zmax::value_to_json
json::node_t * value_to_json(value_t v) const
Definition: zmax.hh:267
awali::sttc::zmax::rdiv
static value_t rdiv(const value_t l, const value_t r)
Definition: zmax.hh:78
b.hh
awali::sttc::zmax::conv
static value_t conv(std::istream &stream)
Definition: zmax.hh:169
awali::sttc::zmax
The Z-max-plus semiring.
Definition: zmax.hh:40
stream.hh
awali::sttc::zmax::is_special
constexpr static bool is_special(value_t)
Definition: zmax.hh:123
fwd.hh
awali::sttc::b
The Boolean semring.
Definition: b.hh:38
awali::TOPS
@ TOPS
Definition: enums.hh:165
awali::sttc::zmax::sname
static std::string sname()
Definition: zmax.hh:45
weightset.hh
awali::sttc::zmax::value_from_json
static value_t value_from_json(json::node_t const *p)
Definition: zmax.hh:243
awali::json::node_t::to_int
virtual int to_int() const
Coerces this node_t to int.
Definition: node.hh:318
enums.hh
awali::sttc::require
void require(bool b, Args &&... args)
If b is not verified, raise an error with args as message.
Definition: raise.hh:55
awali::json::coercion_exception
Exception used when trying to coerce a node to a given type.
Definition: node.hh:140
awali::sttc::rat::to_string
std::string to_string(identities i)
awali::json::node_t
Definition: node.hh:191
awali::sttc::zmax::make
static zmax make(std::istream &is)
Build from the description in is.
Definition: zmax.hh:56
awali::json::int_t
Definition: node.hh:482
awali::parse_exception
Exceptions thrown during parsing.
Definition: parse_exception.hh:26
awali::sttc::str_escape
std::ostream & str_escape(std::ostream &os, const int c)
Definition: escape.hh:30
awali::json::node_t::path_to_root
path_t path_to_root() const
awali::sttc::zmax::is_commutative_semiring
static constexpr bool is_commutative_semiring()
Definition: zmax.hh:140
awali::sttc::zmax::print
static std::ostream & print(const value_t v, std::ostream &o, const std::string &format="text")
Definition: zmax.hh:212
raise.hh
awali::sttc::zmax::print_set
std::ostream & print_set(std::ostream &o, const std::string &format="text") const
Definition: zmax.hh:230
awali::json::object_t
Definition: node.hh:364
awali::sttc::format
auto format(const ValueSet &vs, const typename ValueSet::value_t &v, Args &&... args) -> std::string
Format v via vs.print.
Definition: stream.hh:109
awali::sttc::r
The semiring of floating Numbers.
Definition: r.hh:34
awali::sttc::zmax::conv
static value_t conv(b, b::value_t v)
Definition: zmax.hh:163
awali::sttc::zmax::parse
static value_t parse(const std::string &s, size_t &p)
Definition: zmax.hh:192
awali::sttc::eat
void eat(std::istream &is, char c)
Check lookahead character and advance.
Definition: stream.hh:62
awali::sttc::zmax::star
value_t star(const value_t v) const
Definition: zmax.hh:91
awali::sttc::fail_reading
ATTRIBUTE_NORETURN void fail_reading(std::istream &is, std::string explanation)
Throw an exception after failing to read from is.
Definition: stream.hh:93
awali::json::string_t
Definition: node.hh:525
awali::json::node_t::to_string
virtual std::string to_string() const
Coerces this node_t to an std::string.
Definition: node.hh:328
awali::utils::max
ATTRIBUTE_CONST int max(int a, int b)
Definition: arith.hh:54
awali::utils::hash_value
std::size_t hash_value(const T &v)
Definition: hash.hh:76
awali::sttc::zmax::transpose
static value_t transpose(const value_t v)
Definition: zmax.hh:146
awali::sttc::zmax::star_status
static constexpr star_status_t star_status()
Definition: zmax.hh:143
awali::sttc::zmax::equals
static bool equals(const value_t l, const value_t r)
Definition: zmax.hh:112
awali::sttc::zmax::is_one
static bool is_one(const value_t v)
Definition: zmax.hh:135