← Back to branch summary

~verifypn-cpn/verifypn/partitioning

« back to all changes in this revision

Viewing changes to include/LTL/Structures/BuchiAutomaton.h

  • Committer: tpede16 at aau
  • Date: 2021-04-14 11:51:52 UTC
  • mfrom: (227.5.10 verifypn)
  • Revision ID: tpede16@student.aau.dk-20210414115152-n99btrgc9mmqc02d
Merge with random-fix

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Structures/BuchiAutomaton.h
19
19
#define VERIFYPN_BUCHIAUTOMATON_H
20
20
 
21
21
#include "LTL/LTLToBuchi.h"
 
22
#include "LTL/AlgorithmTypes.h"
22
23
#include <spot/twa/twagraph.hh>
 
24
#include <unordered_map>
 
25
 
 
26
#include <spot/twaalgos/dot.hh>
 
27
#include <spot/twaalgos/hoa.hh>
 
28
#include <spot/twaalgos/neverclaim.hh>
23
29
 
24
30
namespace LTL::Structures {
25
31
    struct BuchiAutomaton {
26
 
        spot::twa_graph_ptr buchi;
 
32
        BuchiAutomaton(spot::twa_graph_ptr buchi, std::unordered_map<int, AtomicProposition> apInfo)
 
33
                : _buchi(std::move(buchi)), ap_info(std::move(apInfo)) {
 
34
            dict = _buchi->get_dict();
 
35
        }
 
36
 
 
37
        spot::twa_graph_ptr _buchi;
27
38
        const std::unordered_map<int, AtomicProposition> ap_info;
 
39
        spot::bdd_dict_ptr dict;
 
40
 
 
41
 
 
42
        void output_buchi(const std::string& file, BuchiOutType type)
 
43
        {
 
44
            std::ofstream fs(file);
 
45
            switch (type) {
 
46
                case BuchiOutType::Dot:
 
47
                    spot::print_dot(fs, _buchi);
 
48
                    break;
 
49
                case BuchiOutType::HOA:
 
50
                    spot::print_hoa(fs, _buchi, "s");
 
51
                    break;
 
52
                case BuchiOutType::Spin:
 
53
                    spot::print_never_claim(fs, _buchi);
 
54
                    break;
 
55
            }
 
56
        }
28
57
    };
29
58
}
30
59