sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

graph preservation properties correctly computed for CTMCs

tempestpy_adaptions
Sebastian Junges 6 years ago
parent
bcde728c3c
commit
8fbc8d56c0
2 changed files with 54 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      src/storm-pars-cli/storm-pars.cpp
  2. 75
      src/storm/analysis/GraphConditions.cpp

5
src/storm-pars-cli/storm-pars.cpp
View File

@ -375,6 +375,11 @@ namespace storm {
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]; boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath()); storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
} }
else if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Ctmc)) {
auto ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*ctmc), parametricSettings.exportResultPath());
}
}); });
} else { } else {
STORM_LOG_TRACE("Sampling the model at given points."); STORM_LOG_TRACE("Sampling the model at given points.");

75
src/storm/analysis/GraphConditions.cpp
View File

@ -56,47 +56,70 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) { void ConstraintCollector<ValueType>::process(storm::models::sparse::Model<ValueType> const& model) {
for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
auto const& transition = *transitionIt;
sum += transition.getValue();
if (!storm::utility::isConstant(transition.getValue())) {
auto const& transitionVars = transition.getValue().gatherVariables();
variableSet.insert(transitionVars.begin(), transitionVars.end());
// Assert: 0 <= transition <= 1
if (model.getType() != storm::models::ModelType::Ctmc) {
for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) {
auto const& transition = *transitionIt;
sum += transition.getValue();
if (!storm::utility::isConstant(transition.getValue())) {
auto const& transitionVars = transition.getValue().gatherVariables();
variableSet.insert(transitionVars.begin(), transitionVars.end());
// Assert: 0 <= transition <= 1
if (transition.getValue().denominator().isConstant()) {
assert(transition.getValue().denominator().constantPart() != 0);
if (transition.getValue().denominator().constantPart() > 0) {
// Assert: nom <= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
// Assert: nom >= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (transition.getValue().denominator().constantPart() < 0) {
// Assert nom >= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
// Assert: nom <= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
}
} else {
// Assert: denom != 0
wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
// Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ), typename ConstraintType<ValueType>::val(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ));
// TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0
}
// Assert: transition > 0
graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
}
}
STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!storm::utility::isConstant(sum)) {
// Assert: sum == 1
wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ);
}
}
} else {
for (auto const& transition : model.getTransitionMatrix()) {
if(!transition.getValue().isConstant()) {
if (transition.getValue().denominator().isConstant()) { if (transition.getValue().denominator().isConstant()) {
assert(transition.getValue().denominator().constantPart() != 0); assert(transition.getValue().denominator().constantPart() != 0);
if (transition.getValue().denominator().constantPart() > 0) { if (transition.getValue().denominator().constantPart() > 0) {
// Assert: nom <= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::LEQ);
// Assert: nom >= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ); wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
} else if (transition.getValue().denominator().constantPart() < 0) { } else if (transition.getValue().denominator().constantPart() < 0) {
// Assert nom >= denom
wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomialWithCoefficient(), storm::CompareRelation::GEQ);
// Assert: nom <= 0
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ); wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else { } else {
STORM_LOG_ASSERT(false, "Denominator must not equal 0.");
assert(false); // Should fail before.
} }
} else { } else {
// Assert: denom != 0
wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ); wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
// Assert: transition >= 0 <==> if denom > 0 then nom >= 0 else nom <= 0
wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType<ValueType>::val(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::GREATER), typename ConstraintType<ValueType>::val(transition. sp/tempest - resources/3rdparty/xercesc-3.1.2/CREDITS at 692ded94cfbe7612696a470cf7ef536a9b208e6f - tempest - Gitea: Git with a cup of tea
sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
6154 Commits
1 Branch
0 Tags
187 MiB
 
 
 
 
Tree: 692ded94cf
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '692ded94cf'
${ noResults }
tempest/resources/3rdparty/xercesc-3.1.2/CREDITS

144 lines
2.0 KiB
Raw Blame History

The following people (in no particular order) have contributed to the
development of the Xerces-C++ source code.
Nadav Aharoni
Curt Arnold
Edward Avis
Anupam Bagchi
Torbjörn Bäckström
Abe Backus
Frank Balluffi
Matthew Baker
Devin Barnhart
James Berry
David Bertoni
John Bellardo
Arundhati Bhowmick
Joanne Bogart
Michael Boos
Edward Bortner
Sean Bright
Phil Brown
Robert Buck
Scott Cantor
David Cargill
Chris Cates
Sumit Chawla
Nick Chiang
Chih Hsiang Chou
Radovan Chytracek
Hiram Clawson
John Clayton
Todd Collins
Nathan Codding
Michael Crawford
Murray Cumming
Zeid Derhally
James Devries
Ailian Ding
Steve Dulin
David Earlam
Helmut Eiken
Mark Everline
Andrew Fang
Simon Fell
Paul Ferguson
Greg Franks
Pierpaolo Fumagalli
Syam Gadde
Guido Gagliardi
Gary Gale
Michael Glavassevich
Natalie Gorden
Max Gotlib
Petr Gotthard
Neil Graham
Matthew Hall
Jay Hansen
Susan Hardenbrook
Jeff Harrell
Andrew Hefford
Adam Heinz
Andy Heninger
John Hibbert
William L. Hopper
Michael Huedepohl
Anders Hybertz
Rahul Jain
Tom Jordahl
Christopher Just
Martin Kalen
Joe Kesselman
Artur Klauser
Bob Kline
Richard Ko
Paul Kramer
Volker Krause
Berin Lautenbach
Arnaud LeHors
Andy Levine
Jeff Lewis
James Littlejohn
Ray Logel
Pedro Lopes
Matt Lovett
Sean MacRoibeaird
Alberto Massari
Don Mastrovito
David McCreedy
Shin'ya MORINO
Urs Muff
Jordan Naftolin
Tinny Ng
David Nickerson
Khaled Noaman
Michael Ottati
Anthony O'Dowd
Mike Pawlowski
Kevin Philips
Mike Pogue
Joe Polastre
John Ponzo
Vitaly Prapirny
Shengkai Qu
Gareth Reakes
Jim Reitz
Caroline Rioux
Dean Roddey
John Roper
Dan Rosen
Steven Rosenthal
Erik Rydgren
Markus Scherer
Bill Schindler
Erik Schroeder
Christian Schuhegger
John Smirl
Andrei Smirnov
John Snelson
Gereon Steffens
Jason Stewart
Rick J. Stevens
Roman Sulzhyk
Linda M. Swan
Vasily Tchekalkin
Pieter Van-Dyck
Curtis Walker
John Warrier
Tom Watson
Mark Weaver
Roger Webster
Robert Weir
Axel Weiss
Carolyn Weiss
Kari Whitcomb
Christian Will
Dietrich Wolf
Kirk Wylie
Peter A. Volchek
Grace Yan
Hiramatsu Yoshifumi
PeiYong Zhang
Henry Zongaro
Boris Kolpackov
0