mCRL2
Loading...
Searching...
No Matches
liblts_swap_to_from_probabilistic_lts.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
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//
10// a plain_lts into a probabilistic lts and vice versa. The
11// lts from which the transformation takes place is destroyed.
12
13#ifndef MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H
14#define MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H
15
18
19namespace mcrl2
20{
21namespace lts
22{
23
24namespace detail
25{
26
27template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
31{
32 static_cast<lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic).swap(l_plain);
33
34 if (l_probabilistic.initial_probabilistic_state().size()<=1)
35 {
36 l_plain.set_initial_state(l_probabilistic.initial_probabilistic_state().get());
37 }
38 else
39 {
40 throw mcrl2::runtime_error("Initial state is probabilistic and cannot be transformed into a non probabilistic state.");
41 }
42
43 // Adapt the probabilistic target states to non probabilistic target states.
44 std::size_t transition_number=1;
45 for(transition& t: l_plain.get_transitions())
46 {
47 std::size_t probabilistic_target_state_number=t.to();
48 if (l_probabilistic.probabilistic_state(probabilistic_target_state_number).size()>1)
49 {
50 throw mcrl2::runtime_error("Transition " + std::to_string(transition_number) + " is probabilistic.");
51 }
52 else
53 {
54 t=transition(t.from(), t.label(), l_probabilistic.probabilistic_state(probabilistic_target_state_number).get());
55 }
56 transition_number++;
57 }
58
59
60}
61
62template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
66{
67 static_cast<lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic)=l_plain;
68 l_probabilistic.set_initial_probabilistic_state(PROBABILISTIC_STATE_T(l_plain.initial_state()));
69 for(std::size_t i=0; i<l_plain.num_states(); ++i)
70 {
71 l_probabilistic.add_probabilistic_state(PROBABILISTIC_STATE_T(i));
72 }
73}
74
75} // detail
76} // lts
77} // mcrl2
78
79#endif // MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H
A class that contains a labelled transition system.
Definition lts.h:83
A class that contains a labelled transition system.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
void swap(abstraction &t1, abstraction &t2)
\brief swap overload
void translate_to_probabilistic_lts(const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain, probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic)
void swap_to_non_probabilistic_lts(probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic, lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The file containing the core class for transition systems.