Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitGspnModelBuilder.cpp
Go to the documentation of this file.
1// #include "storm/builder/ExplicitGspnModelBuilder.h"
2//
3// #include "storm/models/sparse/StandardRewardModel.h"
4//
5// #include "storm/utility/macros.h"
6// #include "storm/exceptions/NotImplementedException.h"
7// #include "storm/storage/expressions/ExpressionManager.h"
8// #include "storm-parsers/parser/FormulaParser.h"
9// #include "storm/storage/expressions/ExpressionEvaluator.h"
10//
11// namespace storm {
12// namespace builder {
13//
14// template<typename ValueType>
15// storm::models::sparse::MarkovAutomaton<ValueType> ExplicitGspnModelBuilder<ValueType>::translateGspn(storm::gspn::GSPN const& gspn, std::string
16// const& formula) {
17// // set the given gspn and compute the limits of the net
18// this->gspn = gspn;
19// computeCapacities(gspn);
20//
21// // markings maps markings to their corresponding rowgroups (indices)
22// markings = storm::storage::BitVectorHashMap<uint_fast64_t>(numberOfTotalBits, 100);
23// builder = storm::storage::SparseMatrixBuilder<double>(0, 0, 0, false, true);
24//
25// // add initial marking to todo list
26// auto bitvector = gspn.getInitialMarking(numberOfBits, numberOfTotalBits)->getBitVector();
27// findOrAddBitvectorToMarkings(*bitvector);
28// currentRowIndex = 0;
29//
30// // vector marking markovian states (vector contains an 1 if the state is markovian)
31// storm::storage::BitVector markovianStates(0);
32//
33// // vector containing the exit rates for the markovian states
34// std::vector<ValueType> exitRates;
35//
36//
37// while (!todo.empty()) {
38// // take next element from the todo list
39// auto currentBitvector = todo.front();
40// todo.pop_front();
41// auto currentMarking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, *currentBitvector);
42//
43// // increment list of states by one
44// markovianStates.resize(markovianStates.size() + 1, 0);
45//
46// // create new row group for the current marking
47// builder.newRowGroup(markings.getValue(*currentBitvector));
48//
49// std::cout << "work on: " << *currentBitvector << '\n';
50//
51// auto enabledImmediateTransitions = getEnabledImmediateTransition(currentMarking);
52// if (!enabledImmediateTransitions.empty()) {
53// markovianStates.set(currentRowIndex, 0);
54// exitRates.push_back(0);
55//
56// auto partitions = partitonEnabledImmediateTransitions(currentMarking, enabledImmediateTransitions);
57// addRowForPartitions(partitions, currentMarking);
58// } else {
59//
60// auto enabledTimedTransitions = getEnabledTimedTransition(currentMarking);
61// if (!enabledTimedTransitions.empty()) {
62// markovianStates.set(currentRowIndex, 1);
63//
64// auto accRate = getAccumulatedRate(enabledTimedTransitions);
65// std::cout << "\t\tacc. rate: " << accRate << '\n';
66// exitRates.push_back(accRate);
67//
68// addRowForTimedTransitions(enabledTimedTransitions, currentMarking, accRate);
69// } else {
70// markovianStates.set(currentRowIndex, 1);
71// }
72// }
73// ++currentRowIndex;
74// }
75//
76// auto matrix = builder.build();
77//
78// // create expression manager and add variables from the gspn
79// auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
80// for (auto& place : gspn.getPlaces()) {
81// expressionManager->declareIntegerVariable(place.getName());
82// }
83//
84// // parse formula
85// storm::parser::FormulaParser formulaParser(expressionManager);
86// auto formulaPtr = formulaParser.parseSingleFormulaFromString(formula);
87// auto atomicFormulas = formulaPtr->getAtomicExpressionFormulas();
88//
89// // create empty state labeling
90// storm::models::sparse::StateLabeling labeling(markings.size());
91// storm::expressions::ExpressionEvaluator<double> expressionEvaluator(*expressionManager);
92//
93// std::cout << '\n';
94// std::cout << "build labeling:\n";
95// for (auto& atomicFormula : atomicFormulas) {
96// std::cout << atomicFormula;
97// auto label = atomicFormula->toString();
98// labeling.addLabel(label);
99//
100// for (auto statePair : markings) {
101// auto marking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, statePair.first);
102// for (auto& place : gspn.getPlaces()) {
103// auto variable = expressionManager->getVariable(place.getName());
104// expressionEvaluator.setIntegerValue(variable, marking.getNumberOfTokensAt(place.getID()));
105// }
106// bool hold = expressionEvaluator.asBool(atomicFormula->getExpression());
107// if (hold) {
108// labeling.addLabelToState(label, statePair.second);
109// }
110// }
111//
112// }
113//
114// //auto labeling = getStateLabeling();
115//
116// return storm::models::sparse::MarkovAutomaton<double>(matrix, labeling, markovianStates, exitRates);
117// }
118//
119// template<typename ValueType>
120// void ExplicitGspnModelBuilder<ValueType>::addRowForPartitions(std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>>
121// const& partitions, storm::gspn::Marking const& currentMarking) {
122// for (auto& partition : partitions) {
123// std::cout << "\tnew partition:\n";
124// auto accWeight = getAccumulatedWeight(partition);
125// std::cout << "\t\tacc. weight: " << accWeight << '\n';
126//
127// std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> weights;
128// for (auto& trans : partition) {
129// std::cout << "\t\ttransname: " << trans.getName() << '\n';
130// auto newMarking = trans.fire(currentMarking);
131// std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << '\n';
132//
133// findOrAddBitvectorToMarkings(*newMarking.getBitVector());
134//
135// auto it = weights.find(markings.getValue(*newMarking.getBitVector()));
136// double currentWeight = 0;
137// if (it != weights.end()) {
138// currentWeight = weights.at(markings.getValue(*newMarking.getBitVector()));
139// }
140// currentWeight += trans.getWeight() / accWeight;
141// weights[markings.getValue(*newMarking.getBitVector())] = currentWeight;
142// }
143//
144// addValuesToBuilder(weights);
145// }
146// }
147//
148// template<typename ValueType>
149// void ExplicitGspnModelBuilder<ValueType>::addRowForTimedTransitions(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const&
150// enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) {
151// std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> rates;
152// for (auto& trans : enabledTimedTransitions) {
153// std::cout << "\t\ttransname: " << trans.getName() << '\n';
154// auto newMarking = trans.fire(currentMarking);
155// std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << '\n';
156//
157// findOrAddBitvectorToMarkings(*newMarking.getBitVector());
158//
159// auto it = rates.find(markings.getValue(*newMarking.getBitVector()));
160// double currentWeightRate = 0;
161// if (it != rates.end()) {
162// currentWeightRate = rates.at(markings.getValue(*newMarking.getBitVector()));
163// }
164// currentWeightRate += trans.getRate() / accRate;
165// rates[markings.getValue(*newMarking.getBitVector())] = currentWeightRate;
166//
167// }
168//
169// addValuesToBuilder(rates);
170// }
171//
172// template<typename ValueType>
173// void ExplicitGspnModelBuilder<ValueType>::addValuesToBuilder(std::map<uint_fast64_t , double,
174// storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> const& values) {
175// for (auto& it : values) {
176// std::cout << "\t\tadd value \"" << it.second << "\" to " << getBitvector(it.first) << '\n';
177// builder.addNextValue(currentRowIndex, it.first, it.second);
178// }
179// }
180//
181// template<typename ValueType>
182// std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>>
183// ExplicitGspnModelBuilder<ValueType>::partitonEnabledImmediateTransitions(
184// storm::gspn::Marking const& marking,
185// std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& enabledImmediateTransitions) {
186// decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result;
187//
188// std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> weightedTransitions;
189//
190// for (auto& trans : enabledImmediateTransitions) {
191// if (trans.noWeightAttached()) {
192// decltype(weightedTransitions) singleton;
193// singleton.push_back(trans);
194// result.push_back(singleton);
195// } else {
196// weightedTransitions.push_back(trans);
197// }
198// }
199//
200// if (weightedTransitions.size() != 0) {
201// result.push_back(weightedTransitions);
202// }
203//
204// return result;
205// }
206//
207// template<typename ValueType>
208// double ExplicitGspnModelBuilder<ValueType>::getAccumulatedWeight(std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const&
209// vector) const {
210// double result = 0;
211//
212// for (auto &trans : vector) {
213// result += trans.getWeight();
214// }
215//
216// return result;
217// }
218//
219// template<typename ValueType>
220// void ExplicitGspnModelBuilder<ValueType>::computeCapacities(storm::gspn::GSPN const& gspn) {
221// uint_fast64_t sum = 0;
222// for (auto& place : gspn.getPlaces()) {//TODO
223// numberOfBits[place.getID()] = 1;
224// sum += numberOfBits[place.getID()];
225// }
226//
227// // compute next multiple of 64
228// uint_fast64_t rem = sum % 64;
229// numberOfTotalBits = sum + 64 - rem;
230// }
231//
232// template<typename ValueType>
233// std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledTimedTransition(
234// storm::gspn::Marking const& marking) {
235// std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>>result;
236//
237// uint_fast64_t highestSeenPriority = 0;
238//
239// for (auto& trans : gspn.getTimedTransitions()) {
240// if (trans.isEnabled(marking)) {
241// if (trans.getPriority() > highestSeenPriority) {
242// highestSeenPriority = trans.getPriority();
243// result.clear();
244// }
245// result.push_back(trans);
246// }
247// }
248//
249// return result;
250// }
251//
252// template<typename ValueType>
253// std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledImmediateTransition(
254// storm::gspn::Marking const& marking) {
255// std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>result;
256//
257// uint_fast64_t highestSeenPriority = 0;
258//
259// for (auto& trans : gspn.getImmediateTransitions()) {
260// if (trans.isEnabled(marking)) {
261// if (trans.getPriority() > highestSeenPriority) {
262// highestSeenPriority = trans.getPriority();
263// result.clear();
264// }
265// result.push_back(trans);
266// }
267// }
268//
269// return result;
270// }
271//
272// template<typename ValueType>
273// double ExplicitGspnModelBuilder<ValueType>::getAccumulatedRate(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& vector) {
274// double result = 0;
275// for (auto trans : vector) {
276// result += trans.getRate();
277// }
278//
279// return result;
280// }
281//
282// template<typename ValueType>
283// storm::storage::BitVector ExplicitGspnModelBuilder<ValueType>::getBitvector(uint_fast64_t const& index) {
284// for (auto it = markings.begin(); it != markings.end(); ++it) {
285// if (std::get<1>(*it) == index) {
286// return std::get<0>(*it);
287// }
288// }
289// return storm::storage::BitVector();
290// }
291//
292// template<typename ValueType>
293// uint_fast64_t ExplicitGspnModelBuilder<ValueType>::findOrAddBitvectorToMarkings(storm::storage::BitVector const &bitvector) {
294// auto index = markings.findOrAdd(bitvector, nextRowGroupIndex);
295//
296// if (index == nextRowGroupIndex) {
297// // bitvector was not already in the map
298// ++nextRowGroupIndex;
299// // bitvector was also never in the todo list
300// todo.push_back(std::make_shared<storm::storage::BitVector>(bitvector));
301// }
302// return index;
303// }
304//
305// template<typename ValueType>
306// storm::models::sparse::StateLabeling ExplicitGspnModelBuilder<ValueType>::getStateLabeling() const {
307// storm::models::sparse::StateLabeling labeling(markings.size());
308//
309// std::map<uint_fast64_t , std::string> idToName;
310// for (auto& place : gspn.getPlaces()) {
311// idToName[place.getID()] = place.getName();
312// labeling.addLabel(place.getName());
313// }
314//
315// auto it = markings.begin();
316// for ( ; it != markings.end() ; ++it) {
317// auto bitvector = std::get<0>(*it);
318// storm::gspn::Marking marking(gspn.getNumberOfPlaces(), numberOfBits, bitvector);
319// for (auto i = 0; i < marking.getNumberOfPlaces(); i++) {
320// if (marking.getNumberOfTokensAt(i) > 0) {
321// std::cout << i << '\n';
322// labeling.addLabelToState(idToName.at(i), i);
323// }
324// }
325// }
326//
327// return labeling;
328// }
329//
330// template class ExplicitGspnModelBuilder<double>;
331// }
332// }