hoa.cc 21.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
// Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#include <ostream>
#include <sstream>
25
#include <cstring>
26
#include <map>
27
28
29
30
31
32
33
34
35
#include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/reachiter.hh>
#include <spot/misc/escape.hh>
#include <spot/misc/bddlt.hh>
#include <spot/misc/minato.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/tl/formula.hh>
36
#include <spot/kripke/fairkripke.hh>
37
38
39
40
41

namespace spot
{
  namespace
  {
42
    struct metadata final
43
44
45
46
47
48
49
50
    {
      // Assign a number to each atomic proposition.
      typedef std::map<int, unsigned> ap_map;
      ap_map ap;
      typedef std::vector<int> vap_t;
      vap_t vap;

      std::vector<bool> common_acc;
51
      bool has_state_acc;
52
53
      bool is_complete;
      bool is_deterministic;
54
      bool is_colored;
55
      bool use_implicit_labels;
56
      bool use_state_labels = true;
57
      bdd all_ap;
58
59
60
61
62
63

      // Label support: the set of all conditions occurring in the
      // automaton.
      typedef std::map<bdd, std::string, bdd_less_than> sup_map;
      sup_map sup;

64
      metadata(const const_twa_graph_ptr& aut, bool implicit,
65
               bool state_labels)
66
      {
67
68
69
        check_det_and_comp(aut);
        use_implicit_labels = implicit && is_deterministic && is_complete;
        use_state_labels &= state_labels;
70
        number_all_ap(aut);
71
72
73
      }

      std::ostream&
74
      emit_acc(std::ostream& os, acc_cond::mark_t b)
75
      {
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
        // FIXME: We could use a cache for this.
        if (b == 0U)
          return os;
        os << " {";
        bool notfirst = false;
        for (auto v: b.sets())
          {
            if (notfirst)
              os << ' ';
            else
              notfirst = true;
            os << v;
          }
        os << '}';
        return os;
91
92
      }

93
      void check_det_and_comp(const const_twa_graph_ptr& aut)
94
      {
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
        std::string empty;

        unsigned ns = aut->num_states();
        bool deterministic = true;
        bool complete = true;
        bool state_acc = true;
        bool nodeadend = true;
        bool colored = aut->num_sets() >= 1;
        for (unsigned src = 0; src < ns; ++src)
          {
            bdd sum = bddfalse;
            bdd available = bddtrue;
            bool st_acc = true;
            bool notfirst = false;
            acc_cond::mark_t prev = 0U;
            bool has_succ = false;
            bdd lastcond = bddfalse;
            for (auto& t: aut->out(src))
              {
                if (has_succ)
                  use_state_labels &= lastcond == t.cond;
                else
                  lastcond = t.cond;
                if (complete)
                  sum |= t.cond;
                if (deterministic)
                  {
                    if (!bdd_implies(t.cond, available))
                      deterministic = false;
                    else
                      available -= t.cond;
                  }
                sup.insert(std::make_pair(t.cond, empty));
                if (st_acc)
                  {
                    if (notfirst && prev != t.acc)
                      {
                        st_acc = false;
                      }
                    else
                      {
                        notfirst = true;
                        prev = t.acc;
                      }
                  }
                if (colored)
                  {
                    auto a = t.acc;
                    if (!a || a.remove_some(1))
                      colored = false;
                  }
                has_succ = true;
              }
            nodeadend &= has_succ;
            if (complete)
              complete &= sum == bddtrue;
            common_acc.push_back(st_acc);
            state_acc &= st_acc;
          }
        is_deterministic = deterministic;
        is_complete = complete;
        has_state_acc = state_acc;
        // If the automaton has state-based acceptance and contain
        // some states without successors do not declare it as
        // colored.
        is_colored = colored && (!has_state_acc || nodeadend);
        // If the automaton declares that it is deterministic or
        // state-based, make sure that it really is.
        assert(deterministic || aut->prop_deterministic() != true);
        assert(state_acc || aut->prop_state_acc() != true);
165
166
      }

167
      void number_all_ap(const const_twa_graph_ptr& aut)
168
      {
169
170
171
172
173
174
        // Make sure that the automaton uses only atomic propositions
        // that have been registered via twa::register_ap() or some
        // variant.  If that is not the case, it is a bug that should
        // be fixed in the function creating the automaton.  Since
        // that function could be written by the user, throw an
        // exception rather than using an assert().
175
176
177
        bdd all = bddtrue;
        for (auto& i: sup)
          all &= bdd_support(i.first);
178
179
180
181
182
        all_ap = aut->ap_vars();
        if (bdd_exist(all, all_ap) != bddtrue)
          throw std::runtime_error("print_hoa(): automaton uses "
                                   "unregistered atomic propositions");
        all = all_ap;
183
184
185
186
187
188

        while (all != bddtrue)
          {
            int v = bdd_var(all);
            all = bdd_high(all);
            ap.insert(std::make_pair(v, vap.size()));
189
            vap.emplace_back(v);
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
          }

        if (use_implicit_labels)
          return;

        for (auto& i: sup)
          {
            bdd cond = i.first;
            if (cond == bddtrue)
              {
                i.second = "t";
                continue;
              }
            if (cond == bddfalse)
              {
                i.second = "f";
                continue;
              }
            std::ostringstream s;
            bool notfirstor = false;

            minato_isop isop(cond);
            bdd cube;
            while ((cube = isop.next()) != bddfalse)
              {
                if (notfirstor)
                  s << " | ";
                bool notfirstand = false;
                while (cube != bddtrue)
                  {
                    if (notfirstand)
                      s << '&';
                    else
                      notfirstand = true;
                    bdd h = bdd_high(cube);
                    if (h == bddfalse)
                      {
                        s << '!' << ap[bdd_var(cube)];
                        cube = bdd_low(cube);
                      }
                    else
                      {
                        s << ap[bdd_var(cube)];
                        cube = h;
                      }
                  }
                notfirstor = true;
              }
            i.second = s.str();
          }
240
241
242
243
244
      }
    };

  }

245
246
  enum hoa_acceptance
    {
247
248
249
250
      Hoa_Acceptance_States,        /// state-based acceptance if
                                /// (globally) possible
                                /// transition-based acceptance
                                /// otherwise.
251
252
253
      Hoa_Acceptance_Transitions, /// transition-based acceptance globally
      Hoa_Acceptance_Mixed    /// mix state-based and transition-based
    };
254

255
  static std::ostream&
256
  print_hoa(std::ostream& os,
257
258
                const const_twa_graph_ptr& aut,
                const char* opt)
259
  {
260
261
262
    bool newline = true;
    hoa_acceptance acceptance = Hoa_Acceptance_States;
    bool implicit_labels = false;
263
    bool verbose = false;
264
    bool state_labels = false;
265
    bool v1_1 = false;
266
267
268

    if (opt)
      while (*opt)
269
270
271
        {
          switch (char c = *opt++)
            {
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
            case '1':
              if (opt[0] == '.' && opt[1] == '1')
                {
                  v1_1 = true;
                  opt += 2;
                }
              else if (opt[0] == '.' && opt[1] == '0')
                {
                  v1_1 = false;
                  opt += 2;
                }
              else
                {
                  v1_1 = false;
                }
              break;
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
            case 'i':
              implicit_labels = true;
              break;
            case 'k':
              state_labels = true;
              break;
            case 'l':
              newline = false;
              break;
            case 'm':
              acceptance = Hoa_Acceptance_Mixed;
              break;
            case 's':
              acceptance = Hoa_Acceptance_States;
              break;
            case 't':
              acceptance = Hoa_Acceptance_Transitions;
              break;
            case 'v':
              verbose = true;
              break;
            default:
              throw std::runtime_error
                (std::string("unknown option for print_hoa(): ") + c);
            }
        }
314

315
    metadata md(aut, implicit_labels, state_labels);
316

317
    if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
318
      acceptance = Hoa_Acceptance_Transitions;
319

320
    unsigned num_states = aut->num_states();
321
    unsigned init = aut->get_init_state_number();
322
323

    const char nl = newline ? '\n' : ' ';
324
    os << (v1_1 ? "HOA: v1.1" : "HOA: v1") << nl;
325
    auto n = aut->get_named_prop<std::string>("automaton-name");
326
    if (n)
327
      escape_str(os << "name: \"", *n) << '"' << nl;
328
    unsigned nap = md.vap.size();
329
    os << "States: " << num_states << nl
330
       << "Start: " << init << nl
331
       << "AP: " << nap;
332
    auto d = aut->get_dict();
333
    for (auto& i: md.vap)
334
      escape_str(os << " \"", d->bdd_map[i].f.ap_name()) << '"';
335
    os << nl;
336

337
    unsigned num_acc = aut->num_sets();
338
    acc_cond::acc_code acc_c = aut->acc().get_acceptance();
339
    if (aut->acc().is_generalized_buchi())
340
      {
341
342
343
344
345
346
347
        if (aut->acc().is_all())
          os << "acc-name: all";
        else if (aut->acc().is_buchi())
          os << "acc-name: Buchi";
        else
          os << "acc-name: generalized-Buchi " << num_acc;
        os << nl;
348
      }
349
350
    else if (aut->acc().is_generalized_co_buchi())
      {
351
352
353
354
355
356
357
        if (aut->acc().is_none())
          os << "acc-name: none";
        else if (aut->acc().is_co_buchi())
          os << "acc-name: co-Buchi";
        else
          os << "acc-name: generalized-co-Buchi " << num_acc;
        os << nl;
358
359
360
      }
    else
      {
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
        int r = aut->acc().is_rabin();
        assert(r != 0);
        if (r > 0)
          {
            os << "acc-name: Rabin " << r << nl;
            // Force the acceptance to remove any duplicate sets, and
            // make sure it is correctly ordered.
            acc_c = acc_cond::acc_code::rabin(r);
          }
        else
          {
            r = aut->acc().is_streett();
            assert(r != 0);
            if (r > 0)
              {
                os << "acc-name: Streett " << r << nl;
                // Force the acceptance to remove any duplicate sets, and
                // make sure it is correctly ordered.
                acc_c = acc_cond::acc_code::streett(r);
              }
            else
              {
                std::vector<unsigned> pairs;
                if (aut->acc().is_generalized_rabin(pairs))
                  {
                    os << "acc-name: generalized-Rabin " << pairs.size();
                    for (auto p: pairs)
                      os << ' ' << p;
                    os << nl;
                    // Force the acceptance to remove any duplicate
                    // sets, and make sure it is correctly ordered.
                    acc_c = acc_cond::acc_code::generalized_rabin(pairs.begin(),
                                                                  pairs.end());
                  }
                else
                  {
                    bool max = false;
                    bool odd = false;
                    if (aut->acc().is_parity(max, odd))
                      os << "acc-name: parity "
                         << (max ? "max " : "min ")
                         << (odd ? "odd " : "even ")
                         << num_acc << nl;
                  }
              }
          }
407
      }
408
    os << "Acceptance: " << num_acc << ' ';
409
    os << acc_c;
410
    os << nl;
411
    os << "properties:";
412
413
414
415
416
    // Make sure the property line is not too large,
    // otherwise our test cases do not fit in 80 columns...
    unsigned prop_len = 60;
    auto prop = [&](const char* str)
      {
417
418
419
420
421
422
423
424
425
426
427
        if (newline)
          {
            auto l = strlen(str);
            if (prop_len < l)
              {
                prop_len = 60;
                os << "\nproperties:";
              }
            prop_len -= l;
          }
        os << str;
428
      };
429
430
431
432
433
434
435
    // We do not support alternating automata so far, and it's
    // probable that nobody cares about the "no-univ-branch"
    // properties.  The "univ-branch" properties seems more important
    // to announce that the automaton might not be parsable by tools
    // that do not support alternating automata.
    if (verbose)
      prop(" no-univ-branch");
436
    implicit_labels = md.use_implicit_labels;
437
    state_labels = md.use_state_labels;
438
    if (implicit_labels)
439
      prop(" implicit-labels");
440
441
    else if (state_labels)
      prop(" state-labels explicit-labels");
442
    else
443
      prop(" trans-labels explicit-labels");
444
    if (acceptance == Hoa_Acceptance_States)
445
      prop(" state-acc");
446
    else if (acceptance == Hoa_Acceptance_Transitions)
447
      prop(" trans-acc");
448
449
    if (md.is_colored)
      prop(" colored");
450
451
    else if (verbose && v1_1)
      prop(" !colored");
452
    if (md.is_complete)
453
      prop(" complete");
454
455
    else if (v1_1)
      prop(" !complete");
456
    if (md.is_deterministic)
457
      prop(" deterministic");
458
459
    else if (v1_1)
      prop(" !deterministic");
460
461
462
463
464
465
    // Deterministic automata are also unambiguous, so writing both
    // properties seems redundant.  People working on unambiguous
    // automata are usually concerned about non-deterministic
    // unambiguous automata.  So do not mention "unambiguous"
    // in the case of deterministic automata.
    if (aut->prop_unambiguous() && (verbose || !md.is_deterministic))
466
      prop(" unambiguous");
467
468
    else if (v1_1 && !aut->prop_unambiguous())
      prop(" !unambiguous");
469
    if (aut->prop_stutter_invariant())
470
      prop(" stutter-invariant");
471
    if (!aut->prop_stutter_invariant())
472
473
474
475
476
477
      {
        if (v1_1)
          prop(" !stutter-invariant");
        else
          prop(" stutter-sensitive");
      }
478
479
    if (aut->prop_terminal())
      prop(" terminal");
480
    if (aut->prop_weak() && (verbose || aut->prop_terminal() != true))
481
      prop(" weak");
482
    if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
483
      prop(" inherently-weak");
484
    if (v1_1 && !aut->prop_terminal() && (verbose || aut->prop_weak() != false))
485
      prop(" !terminal");
486
487
    if (v1_1 && !aut->prop_weak() && (verbose ||
                                      aut->prop_inherently_weak() != false))
488
489
490
      prop(" !weak");
    if (v1_1 && !aut->prop_inherently_weak())
      prop(" !inherently-weak");
491
    os << nl;
492

493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
    // highlighted states and edges are only output in the 1.1 format,
    // because we use a dot in the header name.
    if (v1_1)
      {
        if (auto hstates = aut->get_named_prop
            <std::map<unsigned, unsigned>>("highlight-states"))
          {
            os << "spot.highlight.states:";
            for (auto& p: *hstates)
              os << ' ' << p.first << ' ' << p.second;
            os << nl;
          }
        if (auto hedges = aut->get_named_prop
            <std::map<unsigned, unsigned>>("highlight-edges"))
          {
508
509
510
511
512
513
514
515
516
517
518
519
520
521
            // Numbering edges is a delicate process.  The
            // "highlight-edges" property uses edges numbers that are
            // indices in the "edges" vector.  However these edges
            // need not be sorted.  When edges are output in HOA, they
            // are output with increasing source state number, and the
            // edges number expected in the HOA file should use that
            // order.  So we need to make a first pass on the
            // automaton to number all edges as they will be output.
            unsigned maxedge = aut->edge_vector().size();
            std::vector<unsigned> renum(maxedge);
            unsigned edge = 0;
            for (unsigned i = 0; i < num_states; ++i)
              for (auto& t: aut->out(i))
                renum[aut->get_graph().index_of_edge(t)] = ++edge;
522
523
            os << "spot.highlight.edges:";
            for (auto& p: *hedges)
524
525
              if (p.first < maxedge) // highlighted edges could come from user
                os << ' ' << renum[p.first] << ' ' << p.second;
526
527
528
529
            os << nl;
          }
      }

530
531
532
533
534
535
    // If we want to output implicit labels, we have to
    // fill a vector with all destinations in order.
    std::vector<unsigned> out;
    std::vector<acc_cond::mark_t> outm;
    if (implicit_labels)
      {
536
537
538
        out.resize(1UL << nap);
        if (acceptance != Hoa_Acceptance_States)
          outm.resize(1UL << nap);
539
540
      }

541
    os << "--BODY--" << nl;
542
    auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
543
544
    for (unsigned i = 0; i < num_states; ++i)
      {
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
        hoa_acceptance this_acc = acceptance;
        if (this_acc == Hoa_Acceptance_Mixed)
          this_acc = (md.common_acc[i] ?
                      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);

        os << "State: ";
        if (state_labels)
          {
            bool output = false;
            for (auto& t: aut->out(i))
              {
                os << '[' << md.sup[t.cond] << "] ";
                output = true;
                break;
              }
            if (!output)
              os << "[f] ";
          }
        os << i;
        if (sn && i < sn->size() && !(*sn)[i].empty())
          os << " \"" << (*sn)[i] << '"';
        if (this_acc == Hoa_Acceptance_States)
          {
            acc_cond::mark_t acc = 0U;
            for (auto& t: aut->out(i))
              {
                acc = t.acc;
                break;
              }
            md.emit_acc(os, acc);
          }
        os << nl;

        if (!implicit_labels && !state_labels)
          {

            for (auto& t: aut->out(i))
              {
                os << '[' << md.sup[t.cond] << "] " << t.dst;
                if (this_acc == Hoa_Acceptance_Transitions)
                  md.emit_acc(os, t.acc);
                os << nl;
              }
          }
        else if (state_labels)
          {
            unsigned n = 0;
            for (auto& t: aut->out(i))
              {
                os << t.dst;
                if (this_acc == Hoa_Acceptance_Transitions)
                  {
                    md.emit_acc(os, t.acc);
                    os << nl;
                  }
                else
                  {
                    ++n;
                    os << (((n & 15) && t.next_succ) ? ' ' : nl);
                  }
              }
          }
        else
          {
            for (auto& t: aut->out(i))
              {
                bdd cond = t.cond;
                while (cond != bddfalse)
                  {
                    bdd one = bdd_satoneset(cond, md.all_ap, bddfalse);
                    cond -= one;
                    unsigned level = 1;
                    unsigned pos = 0U;
                    while (one != bddtrue)
                      {
                        bdd h = bdd_high(one);
                        if (h == bddfalse)
                          {
                            one = bdd_low(one);
                          }
                        else
                          {
                            pos |= level;
                            one = h;
                          }
                        level <<= 1;
                      }
                    out[pos] = t.dst;
                    if (this_acc != Hoa_Acceptance_States)
                      outm[pos] = t.acc;
                  }
              }
            unsigned n = out.size();
            for (unsigned i = 0; i < n;)
              {
                os << out[i];
                if (this_acc != Hoa_Acceptance_States)
                  {
                    md.emit_acc(os, outm[i]) << nl;
                    ++i;
                  }
                else
                  {
                    ++i;
                    os << (((i & 15) && i < n) ? ' ' : nl);
                  }
              }
          }
653
      }
654
    os << "--END--";                // No newline.  Let the caller decide.
655
656
657
658
    return os;
  }

  std::ostream&
659
  print_hoa(std::ostream& os,
660
661
            const const_twa_ptr& aut,
            const char* opt)
662
  {
663

664
    auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
665
    if (!a)
666
      a = make_twa_graph(aut, twa::prop_set::all());
667

668
669
    // for Kripke structures, automatically append "k" to the options.
    char* tmpopt = nullptr;
670
    if (std::dynamic_pointer_cast<const fair_kripke>(aut))
671
      {
672
673
674
675
676
677
        unsigned n = opt ? strlen(opt) : 0;
        tmpopt = new char[n + 2];
        if (opt)
          strcpy(tmpopt, opt);
        tmpopt[n] = 'k';
        tmpopt[n + 1] = 0;
678
679
680
681
      }
    print_hoa(os, a, tmpopt ? tmpopt : opt);
    delete[] tmpopt;
    return os;
682
683
684
  }

}