mCRL2
Loading...
Searching...
No Matches
lts_load.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_LTS_DETAIL_LTS_LOAD_H
13#define MCRL2_LTS_DETAIL_LTS_LOAD_H
14
17#include "mcrl2/lts/lts_io.h"
18
19namespace mcrl2 {
20
21namespace lts {
22
23namespace detail {
24
25inline
26void add_options(utilities::interface_description& desc)
27{
28 desc.add_option("data", utilities::make_file_argument("FILE"),
29 "use FILE as the data and action specification. "
30 "FILE must be a .mcrl2 file which does not contain an init clause. ", 'D');
31
32 desc.add_option("lps", utilities::make_file_argument("FILE"),
33 "use FILE for the data and action specification. "
34 "FILE must be a .lps file. ", 'l');
35
36 desc.add_option("mcrl2", utilities::make_file_argument("FILE"),
37 "use FILE as the data and action specification for the LTS. "
38 "FILE must be a .mcrl2 file. ", 'm');
39}
40
41// Load an LTS from ltsfilename, with additional files specified in the command line parser.
42// TODO: this incomprehensible interface for loading LTSs needs improvement.
43template <class LTS_TYPE>
44void load_lts(const utilities::command_line_parser& parser, const std::string& ltsfilename, LTS_TYPE& result)
45{
46 data_file_type_t data_file_type = data_file_type_t::none_e;
47 std::string data_file;
48
49 if (parser.options.count("data"))
50 {
51 if (1 < parser.options.count("data"))
52 {
53 mCRL2log(log::warning) << "Multiple data specification files are specified; can only use one.\n";
54 }
55 data_file_type = data_file_type_t::data_e;
56 data_file = parser.option_argument("data");
57 }
58
59 if (parser.options.count("lps"))
60 {
61 if (1 < parser.options.count("lps") || data_file_type != data_file_type_t::none_e)
62 {
63 mCRL2log(log::warning) << "Multiple data specification files are specified; can only use one.\n";
64 }
65
66 data_file_type = data_file_type_t::lps_e;
67 data_file = parser.option_argument("lps");
68 }
69
70 if (parser.options.count("mcrl2"))
71 {
72 if (1 < parser.options.count("mcrl2") || data_file_type != data_file_type_t::none_e)
73 {
74 mCRL2log(log::warning) << "Multiple data specification files are specified; can only use one.\n";
75 }
76
77 data_file_type = data_file_type_t::mcrl2_e;
78 data_file = parser.option_argument("mcrl2");
79 }
80
81 lts_type input_type = detail::guess_format(ltsfilename);
82 load_lts(result, ltsfilename, input_type, data_file_type, data_file);
83}
84
85// extracts a specification from an LTS
86template <class LTS_TYPE>
88{
90 data::variable process_parameter("x", data::sort_pos::pos());
91 data::variable_list process_parameters({ process_parameter });
92 std::set<data::variable> global_variables;
93 // Add a single delta.
95 lps::stochastic_linear_process lps(process_parameters, deadlock_summands, lps::stochastic_action_summand_vector());
96
98 if constexpr (!(LTS_TYPE::is_probabilistic_lts))
99 {
102 }
103 else // The initial state is probabilistic.
104 {
105 const typename LTS_TYPE::probabilistic_state_t& init = l.initial_probabilistic_state();
106 if (init.size()<=1)
107 {
110 }
111 else
112 {
113 data::variable stoch_var("stoch_var", data::sort_pos::pos());
116 std::size_t count=init.size();
117 for(typename LTS_TYPE::probabilistic_state_t::const_reverse_iterator i=init.rbegin(); i!=init.rend(); ++i)
118 {
119 distribution=data::if_(data::equal_to(stoch_var,data::sort_pos::pos(count)), i->probability(), distribution);
121 count--;
122 }
125 distribution));
126
127 }
128 }
129 return lps::stochastic_specification(l.data(), l.action_label_declarations(), global_variables, lps, initial_process);
130}
131
132} // namespace detail
133
134} // namespace lts
135
136} // namespace mcrl2
137
138#endif // MCRL2_LTS_DETAIL_LTS_LOAD_H
Read-only balanced binary tree of terms.
\brief A data variable
Definition variable.h:28
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
\brief A stochastic distribution
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This include file contains routines to read and write labelled transitions from and to files and from...
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
data_expression & real_zero()
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
@ warning
Definition logger.h:32
std::vector< stochastic_action_summand > stochastic_action_summand_vector
\brief vector of stochastic_action_summands
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
lps::stochastic_specification extract_specification(const LTS_TYPE &l)
Definition lts_load.h:87
void load_lts(const utilities::command_line_parser &parser, const std::string &ltsfilename, LTS_TYPE &result)
Definition lts_load.h:44
void add_options(utilities::interface_description &desc)
Definition lts_load.h:26
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
data_file_type_t
Type for data files that contain extra information for an lts in .aut or .fsm format....
Definition lts_io.h:33
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Contains a number of auxiliary functions to recognize reals.
add your file description here.