Line data Source code
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 : // 9 : /// \file mcrl2/pbes/untyped_pbes.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_UNTYPED_PBES_H 13 : #define MCRL2_PBES_UNTYPED_PBES_H 14 : 15 : #include "mcrl2/data/untyped_data_specification.h" 16 : #include "mcrl2/pbes/pbes.h" 17 : 18 : namespace mcrl2 { 19 : 20 : namespace pbes_system { 21 : 22 : struct untyped_pbes 23 : { 24 : data::untyped_data_specification dataspec; 25 : data::variable_list global_variables; 26 : std::vector<pbes_equation> equations; 27 : propositional_variable_instantiation initial_state; 28 : 29 467 : pbes construct_pbes() const 30 : { 31 467 : pbes result; 32 467 : result.data() = dataspec.construct_data_specification(); 33 467 : result.global_variables() = std::set<data::variable>(global_variables.begin(), global_variables.end()); 34 467 : result.equations() = equations; 35 467 : result.initial_state() = initial_state; 36 467 : return result; 37 0 : } 38 : }; 39 : 40 : } // namespace pbes_system 41 : 42 : } // namespace mcrl2 43 : 44 : #endif // MCRL2_PBES_UNTYPED_PBES_H