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

Added AND_EXISTS to sylvan+RationalFunction 

Former-commit-id: 7b462145cf
tempestpy_adaptions
PBerger 8 years ago
parent
9eee889539
commit
0717ffe053
3 changed files with 126 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 88
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
  2. 7
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
  3. 37
      test/functional/storage/SylvanDdTest.cpp

88
resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
View File

@ -10,7 +10,7 @@
#include <sylvan.h>
#include <sylvan_common.h>
/*#include <sylvan_mtbdd_int.h>*/
#include <sylvan_mtbdd_int.h>
#include <sylvan_storm_rational_function.h>
#include <storm_function_wrapper.h>
@ -162,14 +162,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v
{
LOG_I("task_impl_2 to_srf")
if (a == mtbdd_false) {
storm_rational_function_ptr srf_zero = storm_rational_function_get_zero();
MTBDD result = mtbdd_storm_rational_function(srf_zero);
MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_zero());
LOG_O("task_impl_2 to_srf - ZERO")
return result;
}
if (a == mtbdd_true) {
storm_rational_function_ptr srf_one = storm_rational_function_get_one();
MTBDD result = mtbdd_storm_rational_function(srf_one);
MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_one());
LOG_O("task_impl_2 to_srf - ONE")
return result;
}
@ -183,7 +181,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v
TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd)
{
LOG_I("task_impl_1 to_srf")
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0);
}
@ -379,3 +376,82 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p)
return mtbdd_invalid;
(void)p;
}
/**
* Multiply <a> and <b>, and abstract variables <vars> using summation.
* This is similar to the "and_exists" operation in BDDs.
*/
TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b, MTBDD, v)
{
/* Check terminal cases */
/* If v == true, then <vars> is an empty set */
if (v == mtbdd_true) return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times));
/* Try the times operator on a and b */
MTBDD result = CALL(sylvan_storm_rational_function_op_times, &a, &b);
if (result != mtbdd_invalid) {
/* Times operator successful, store reference (for garbage collection) */
mtbdd_refs_push(result);
/* ... and perform abstraction */
result = mtbdd_abstract(result, v, TASK(sylvan_storm_rational_function_abstract_op_plus));
mtbdd_refs_pop(1);
/* Note that the operation cache is used in mtbdd_abstract */
return result;
}
/* Maybe perform garbage collection */
sylvan_gc_test();
/* Check cache. Note that we do this now, since the times operator might swap a and b (commutative) */
if (cache_get3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, &result)) return result;
/* Now, v is not a constant, and either a or b is not a constant */
/* Get top variable */
int la = mtbdd_isleaf(a);
int lb = mtbdd_isleaf(b);
mtbddnode_t na = la ? 0 : GETNODE(a);
mtbddnode_t nb = lb ? 0 : GETNODE(b);
uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na);
uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb);
uint32_t var = va < vb ? va : vb;
mtbddnode_t nv = GETNODE(v);
uint32_t vv = mtbddnode_getvariable(nv);
if (vv < var) {
/* Recursive, then abstract result */
result = CALL(sylvan_storm_rational_function_and_exists, a, b, node_gethigh(v, nv));
mtbdd_refs_push(result);
result = mtbdd_apply(result, result, TASK(sylvan_storm_rational_function_op_plus));
mtbdd_refs_pop(1);
} else {
/* Get cofactors */
MTBDD alow, ahigh, blow, bhigh;
alow = (!la && va == var) ? node_getlow(a, na) : a;
ahigh = (!la && va == var) ? node_gethigh(a, na) : a;
blow = (!lb && vb == var) ? node_getlow(b, nb) : b;
bhigh = (!lb && vb == var) ? node_gethigh(b, nb) : b;
if (vv == var) {
/* Recursive, then abstract result */
mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_function_and_exists, ahigh, bhigh, node_gethigh(v, nv)));
MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_function_and_exists, alow, blow, node_gethigh(v, nv)));
MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(sylvan_storm_rational_function_and_exists)));
result = CALL(mtbdd_apply, low, high, TASK(sylvan_storm_rational_function_op_plus));
mtbdd_refs_pop(2);
} else /* vv > v */ {
/* Recursive, then create node */
mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_function_and_exists, ahigh, bhigh, v));
MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_function_and_exists, alow, blow, v));
MTBDD high = mtbdd_refs_sync(SYNC(sylvan_storm_rational_function_and_exists));
mtbdd_refs_pop(1);
result = mtbdd_makenode(var, low, high);
}
}
/* Store in cache */
cache_put3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, result);
return result;
}

7
resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
View File

@ -92,6 +92,13 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t)
*/
#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0);
/**
* Multiply <a> and <b>, and abstract variables <vars> using summation.
* This is similar to the "and_exists" operation in BDDs.
*/
TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBDD);
#define sylvan_storm_rational_function_and_exists(a, b, vars) CALL(sylvan_storm_rational_function_and_exists, a, b, vars)
#ifdef __cplusplus
}
#endif /* __cplusplus */

37
test/functional/storage/SylvanDdTest.cpp
View File

@ -11,6 +11,9 @@
#include "src/storage/SparseMatrix.h"
#include <memory>
#include <iostream>
TEST(SylvanDd, Constants) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
storm::dd::Add<storm::dd::DdType::Sylvan, double> zero;
@ -106,6 +109,40 @@ TEST(SylvanDd, RationalFunctionConstants) {
EXPECT_EQ(0ul, two.getNonZeroCount());
EXPECT_EQ(1ul, two.getLeafCount());
EXPECT_EQ(1ul, two.getNodeCount());
// The cache that is used in case the underlying type needs a cache.
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>>();
storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> function;
carl::Variable x = carl::freshRealVariable("x");
carl::Variable y = carl::freshRealVariable("y");
carl::Variable z = carl::freshRealVariable("z");
storm::RationalFunction constantOne(1);
storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache));
storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache));
storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache));
storm::RationalFunction constantOneDivTwo(constantOne / constantTwo);
storm::RationalFunction tmpFunctionA(constantOneDivTwo);
tmpFunctionA *= variableZ;
tmpFunctionA /= variableY;
storm::RationalFunction tmpFunctionB(variableX);
tmpFunctionB *= variableY;
//storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y);
storm::RationalFunction rationalFunction(constantTwo);
rationalFunction *= variableX;
rationalFunction += tmpFunctionB;
rationalFunction += tmpFunctionA;
ASSERT_NO_THROW(function = manager->template getConstant<storm::RationalFunction>(rationalFunction));
EXPECT_EQ(0ul, function.getNonZeroCount());
EXPECT_EQ(1ul, function.getLeafCount());
EXPECT_EQ(1ul, function.getNodeCount());
}
TEST(SylvanDd, RationalFunctionEncodingTest) {

Write Preview
Loading…
Cancel
Save