Browse Source
Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games
Former-commit-id: 3a1ecb6b7f
main
dehnert
10 years ago
50 changed files with 2820 additions and 278 deletions
-
15CMakeLists.txt
-
2resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
-
18resources/3rdparty/sylvan/CMakeLists.txt
-
6resources/3rdparty/sylvan/examples/CMakeLists.txt
-
127resources/3rdparty/sylvan/examples/storm.cpp
-
9resources/3rdparty/sylvan/src/CMakeLists.txt
-
206resources/3rdparty/sylvan/src/storm_function_wrapper.cpp
-
37resources/3rdparty/sylvan/src/storm_function_wrapper.h
-
2resources/3rdparty/sylvan/src/sylvan_bdd.c
-
171resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
-
5resources/3rdparty/sylvan/src/sylvan_bdd_storm.h
-
127resources/3rdparty/sylvan/src/sylvan_mtbdd.c
-
2resources/3rdparty/sylvan/src/sylvan_mtbdd.h
-
294resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
-
50resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
-
11resources/3rdparty/sylvan/src/sylvan_obj.cpp
-
9resources/3rdparty/sylvan/src/sylvan_obj.hpp
-
4resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
-
34resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
-
62resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
-
457resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
-
113resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
-
5src/abstraction/AbstractionInformation.cpp
-
1src/abstraction/AbstractionInformation.h
-
9src/abstraction/MenuGame.cpp
-
6src/abstraction/StateSetAbstractor.cpp
-
8src/abstraction/prism/AbstractCommand.cpp
-
8src/abstraction/prism/AbstractModule.cpp
-
11src/abstraction/prism/AbstractProgram.cpp
-
7src/adapters/AddExpressionAdapter.cpp
-
2src/modelchecker/DFTAnalyser.h
-
4src/models/sparse/NondeterministicModel.cpp
-
7src/models/symbolic/Model.cpp
-
7src/models/symbolic/NondeterministicModel.cpp
-
12src/models/symbolic/StochasticTwoPlayerGame.cpp
-
6src/storage/dd/Add.cpp
-
16src/storage/dd/Bdd.cpp
-
25src/storage/dd/DdManager.cpp
-
277src/storage/dd/sylvan/InternalSylvanAdd.cpp
-
14src/storage/dd/sylvan/InternalSylvanAdd.h
-
20src/storage/dd/sylvan/InternalSylvanBdd.cpp
-
38src/storage/dd/sylvan/InternalSylvanDdManager.cpp
-
319src/storage/dd/sylvan/InternalSylvanDdManager.h
-
6src/storage/dd/sylvan/SylvanAddIterator.cpp
-
37src/utility/sylvan.h
-
23test/functional/abstraction/PrismMenuGameTest.cpp
-
223test/functional/storage/CuddDdTest.cpp
-
2test/functional/storage/PrismProgramTest.cpp
-
242test/functional/storage/SylvanDdTest.cpp
-
2test/functional/utility/GraphTest.cpp
@ -0,0 +1,127 @@ |
|||
#ifdef NDEBUG
|
|||
#undef NDEBUG
|
|||
#endif
|
|||
|
|||
#include <assert.h>
|
|||
#include <stdio.h>
|
|||
#include <stdint.h>
|
|||
|
|||
#include <sylvan.h>
|
|||
#include <sylvan_obj.hpp>
|
|||
#include <storm_function_wrapper.h>
|
|||
#include <sylvan_storm_rational_function.h>
|
|||
|
|||
using namespace sylvan; |
|||
|
|||
VOID_TASK_0(storm_rf) |
|||
{ |
|||
Bdd one = Bdd::bddOne(); // the True terminal
|
|||
Bdd zero = Bdd::bddZero(); // the False terminal
|
|||
|
|||
// check if they really are the True/False terminal
|
|||
assert(one.GetBDD() == sylvan_true); |
|||
assert(zero.GetBDD() == sylvan_false); |
|||
|
|||
Bdd a = Bdd::bddVar(0); // create a BDD variable x_0
|
|||
Bdd b = Bdd::bddVar(1); // create a BDD variable x_1
|
|||
|
|||
// check if a really is the Boolean formula "x_0"
|
|||
assert(!a.isConstant()); |
|||
assert(a.TopVar() == 0); |
|||
assert(a.Then() == one); |
|||
assert(a.Else() == zero); |
|||
|
|||
// check if b really is the Boolean formula "x_1"
|
|||
assert(!b.isConstant()); |
|||
assert(b.TopVar() == 1); |
|||
assert(b.Then() == one); |
|||
assert(b.Else() == zero); |
|||
|
|||
// compute !a
|
|||
Bdd not_a = !a; |
|||
|
|||
// check if !!a is really a
|
|||
assert((!not_a) == a); |
|||
|
|||
// compute a * b and !(!a + !b) and check if they are equivalent
|
|||
Bdd a_and_b = a * b; |
|||
Bdd not_not_a_or_not_b = !(!a + !b); |
|||
assert(a_and_b == not_not_a_or_not_b); |
|||
|
|||
// perform some simple quantification and check the results
|
|||
Bdd ex = a_and_b.ExistAbstract(a); // \exists a . a * b
|
|||
assert(ex == b); |
|||
Bdd andabs = a.AndAbstract(b, a); // \exists a . a * b using AndAbstract
|
|||
assert(ex == andabs); |
|||
Bdd univ = a_and_b.UnivAbstract(a); // \forall a . a * b
|
|||
assert(univ == zero); |
|||
|
|||
// alternative method to get the cube "ab" using bddCube
|
|||
BddSet variables = a * b; |
|||
std::vector<unsigned char> vec = {1, 1}; |
|||
assert(a_and_b == Bdd::bddCube(variables, vec)); |
|||
|
|||
// test the bddCube method for all combinations
|
|||
assert((!a * !b) == Bdd::bddCube(variables, std::vector<uint8_t>({0, 0}))); |
|||
assert((!a * b) == Bdd::bddCube(variables, std::vector<uint8_t>({0, 1}))); |
|||
assert((!a) == Bdd::bddCube(variables, std::vector<uint8_t>({0, 2}))); |
|||
assert((a * !b) == Bdd::bddCube(variables, std::vector<uint8_t>({1, 0}))); |
|||
assert((a * b) == Bdd::bddCube(variables, std::vector<uint8_t>({1, 1}))); |
|||
assert((a) == Bdd::bddCube(variables, std::vector<uint8_t>({1, 2}))); |
|||
assert((!b) == Bdd::bddCube(variables, std::vector<uint8_t>({2, 0}))); |
|||
assert((b) == Bdd::bddCube(variables, std::vector<uint8_t>({2, 1}))); |
|||
assert(one == Bdd::bddCube(variables, std::vector<uint8_t>({2, 2}))); |
|||
} |
|||
|
|||
VOID_TASK_1(_main, void*, arg) |
|||
{ |
|||
// Initialize Sylvan
|
|||
// With starting size of the nodes table 1 << 21, and maximum size 1 << 27.
|
|||
// With starting size of the cache table 1 << 20, and maximum size 1 << 20.
|
|||
// Memory usage: 24 bytes per node, and 36 bytes per cache bucket
|
|||
// - 1<<24 nodes: 384 MB
|
|||
// - 1<<25 nodes: 768 MB
|
|||
// - 1<<26 nodes: 1536 MB
|
|||
// - 1<<27 nodes: 3072 MB
|
|||
// - 1<<24 cache: 576 MB
|
|||
// - 1<<25 cache: 1152 MB
|
|||
// - 1<<26 cache: 2304 MB
|
|||
// - 1<<27 cache: 4608 MB
|
|||
sylvan_init_package(1LL<<22, 1LL<<26, 1LL<<22, 1LL<<26); |
|||
|
|||
// Initialize the BDD module with granularity 1 (cache every operation)
|
|||
// A higher granularity (e.g. 6) often results in better performance in practice
|
|||
sylvan_init_bdd(1); |
|||
|
|||
// Now we can do some simple stuff using the C++ objects.
|
|||
CALL(storm_rf); |
|||
|
|||
// Report statistics (if SYLVAN_STATS is 1 in the configuration)
|
|||
sylvan_stats_report(stdout, 1); |
|||
|
|||
// And quit, freeing memory
|
|||
sylvan_quit(); |
|||
|
|||
// We didn't use arg
|
|||
(void)arg; |
|||
} |
|||
|
|||
int |
|||
main (int argc, char *argv[]) |
|||
{ |
|||
int n_workers = 0; // automatically detect number of workers
|
|||
size_t deque_size = 0; // default value for the size of task deques for the workers
|
|||
size_t program_stack_size = 0; // default value for the program stack of each pthread
|
|||
|
|||
// Initialize the Lace framework for <n_workers> workers.
|
|||
lace_init(n_workers, deque_size); |
|||
|
|||
// Spawn and start all worker pthreads; suspends current thread until done.
|
|||
lace_startup(program_stack_size, TASK(_main), NULL); |
|||
|
|||
// The lace_startup command also exits Lace after _main is completed.
|
|||
|
|||
return 0; |
|||
(void)argc; // unused variable
|
|||
(void)argv; // unused variable
|
|||
} |
|||
@ -0,0 +1,206 @@ |
|||
#include "storm_function_wrapper.h"
|
|||
|
|||
#include <cstring>
|
|||
#include <iostream>
|
|||
#include <sstream>
|
|||
#include "src/adapters/CarlAdapter.h"
|
|||
|
|||
#undef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
|
|||
#ifdef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
#define LOG_I(funcName) std::cout << "Entering function " << funcName << std::endl;
|
|||
#define LOG_O(funcName) std::cout << "Leaving function " << funcName << std::endl;
|
|||
#else
|
|||
#define LOG_I(funcName)
|
|||
#define LOG_O(funcName)
|
|||
#endif
|
|||
|
|||
void storm_rational_function_init(storm_rational_function_ptr* a) { |
|||
LOG_I("init") |
|||
#ifdef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
std::cout << "storm_rational_function_init - ptr of old = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; |
|||
#endif
|
|||
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); |
|||
|
|||
if (srf_ptr == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; |
|||
return; |
|||
} |
|||
|
|||
*a = srf_ptr; |
|||
#ifdef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
std::cout << "storm_rational_function_init - ptr of new = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; |
|||
#endif
|
|||
LOG_O("init") |
|||
} |
|||
|
|||
void storm_rational_function_destroy(storm_rational_function_ptr a) { |
|||
LOG_I("destroy") |
|||
delete (storm::RationalFunction*)a; |
|||
LOG_O("destroy") |
|||
} |
|||
|
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
LOG_I("equals") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
LOG_O("equals") |
|||
|
|||
int result = 0; |
|||
if (srf_a == srf_b) { |
|||
result = 1; |
|||
} |
|||
|
|||
#ifdef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
std::cout << "storm_rational_function_equals called with ptr = " << a << " value a = " << srf_a << " and ptr = " << b << " value b = " << srf_b << " result = " << result << "." << std::endl; |
|||
#endif
|
|||
|
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
LOG_I("plus") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; |
|||
return (storm_rational_function_ptr)nullptr; |
|||
} |
|||
|
|||
*result_srf += srf_b; |
|||
|
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
LOG_O("plus") |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
LOG_I("minus") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; |
|||
return (storm_rational_function_ptr)nullptr; |
|||
} |
|||
|
|||
*result_srf -= srf_b; |
|||
|
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
LOG_O("minus") |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
LOG_I("times") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; |
|||
return (storm_rational_function_ptr)nullptr; |
|||
} |
|||
|
|||
*result_srf *= srf_b; |
|||
|
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
LOG_O("times") |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
LOG_I("divide") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; |
|||
return (storm_rational_function_ptr)nullptr; |
|||
} |
|||
|
|||
*result_srf /= srf_b; |
|||
|
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
LOG_O("divide") |
|||
return result; |
|||
} |
|||
|
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { |
|||
LOG_I("hash") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
|
|||
size_t hash = carl::hash_value(srf_a); |
|||
|
|||
#ifdef DEBUG_STORM_FUNCTION_WRAPPER
|
|||
std::cout << "storm_rational_function_hash of value " << srf_a << " is " << hash << std::endl; |
|||
#endif
|
|||
|
|||
uint64_t result = hash ^ seed; |
|||
|
|||
LOG_O("hash") |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { |
|||
LOG_I("negate") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; |
|||
return (storm_rational_function_ptr)nullptr; |
|||
} |
|||
|
|||
*result_srf = -srf_a; |
|||
|
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
LOG_O("negate") |
|||
return result; |
|||
} |
|||
|
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a) { |
|||
LOG_I("isZero") |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
|
|||
if (srf_a.isZero()) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_zero() { |
|||
static storm::RationalFunction zeroFunction(0); |
|||
LOG_I("getZero") |
|||
return (storm_rational_function_ptr)(&zeroFunction); |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_one() { |
|||
static storm::RationalFunction oneFunction(1); |
|||
LOG_I("getOne") |
|||
return (storm_rational_function_ptr)(&oneFunction); |
|||
} |
|||
|
|||
void print_storm_rational_function(storm_rational_function_ptr a) { |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
std::cout << srf_a << std::flush; |
|||
} |
|||
|
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { |
|||
std::stringstream ss; |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
ss << srf_a; |
|||
std::string s = ss.str(); |
|||
fprintf(out, "%s", s.c_str()); |
|||
} |
|||
@ -0,0 +1,37 @@ |
|||
#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
#define SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
|
|||
#include <stdint.h> |
|||
#include <stdio.h> |
|||
|
|||
#ifdef __cplusplus |
|||
extern "C" { |
|||
#endif |
|||
|
|||
typedef void* storm_rational_function_ptr; |
|||
|
|||
// equals, plus, minus, divide, times, create, destroy |
|||
void storm_rational_function_init(storm_rational_function_ptr* a); |
|||
void storm_rational_function_destroy(storm_rational_function_ptr a); |
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); |
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); |
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a); |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_zero(); |
|||
storm_rational_function_ptr storm_rational_function_get_one(); |
|||
|
|||
void print_storm_rational_function(storm_rational_function_ptr a); |
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); |
|||
|
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a); |
|||
|
|||
#ifdef __cplusplus |
|||
} |
|||
#endif |
|||
|
|||
#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
@ -0,0 +1,171 @@ |
|||
/* */ |
|||
|
|||
/** |
|||
* Calculates \exists variables . a |
|||
*/ |
|||
TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, prev_level) |
|||
{ |
|||
int aIsNegated = (a & sylvan_complement) == ((uint64_t)0) ? 0 : 1; |
|||
|
|||
BDD aRegular = (aIsNegated) ? sylvan_not(a) : a; |
|||
|
|||
if (aRegular == sylvan_false) { |
|||
if (aIsNegated) { |
|||
if (sylvan_set_isempty(variables)) { |
|||
//printf("return in preprocessing...2\n"); |
|||
return sylvan_true; |
|||
} else { |
|||
//printf("return in preprocessing...3\n"); |
|||
BDD _v = sylvan_set_next(variables); |
|||
BDD res = CALL(sylvan_existsRepresentative, a, _v, prev_level); |
|||
if (res == sylvan_invalid) { |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res); |
|||
|
|||
BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(GETNODE(variables))), sylvan_false, res); |
|||
if (res1 == sylvan_invalid) { |
|||
sylvan_deref(res); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_deref(res); |
|||
return res1; |
|||
} |
|||
} else { |
|||
return a; |
|||
} |
|||
} else if (sylvan_set_isempty(variables)) { |
|||
//printf("return in preprocessing...4\n"); |
|||
return a; |
|||
} |
|||
/* From now on, f and cube are non-constant. */ |
|||
bddnode_t na = GETNODE(a); |
|||
BDDVAR level = bddnode_getvariable(na); |
|||
|
|||
bddnode_t nv = GETNODE(variables); |
|||
BDDVAR vv = bddnode_getvariable(nv); |
|||
|
|||
//printf("a level %i and cube level %i\n", level, vv); |
|||
|
|||
/* Abstract a variable that does not appear in f. */ |
|||
if (level > vv) { |
|||
BDD _v = sylvan_set_next(variables); |
|||
BDD res = CALL(sylvan_existsRepresentative, a, _v, level); |
|||
if (res == sylvan_invalid) { |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res); |
|||
|
|||
BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); |
|||
|
|||
if (res1 == sylvan_invalid) { |
|||
sylvan_deref(res); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_deref(res); |
|||
|
|||
//printf("return after abstr. var that does not appear in f...\n"); |
|||
return res1; |
|||
} |
|||
|
|||
/* Compute the cofactors of a. */ |
|||
BDD aLow = node_low(a, na); // ELSE |
|||
BDD aHigh = node_high(a, na); // THEN |
|||
|
|||
/* If the two indices are the same, so are their levels. */ |
|||
if (level == vv) { |
|||
BDD _v = sylvan_set_next(variables); |
|||
BDD res1 = CALL(sylvan_existsRepresentative, aLow, _v, level); |
|||
if (res1 == sylvan_invalid) { |
|||
return sylvan_invalid; |
|||
} |
|||
if (res1 == sylvan_true) { |
|||
return sylvan_not(variables); |
|||
} |
|||
sylvan_ref(res1); |
|||
|
|||
BDD res2 = CALL(sylvan_existsRepresentative, aHigh, _v, level); |
|||
if (res2 == sylvan_invalid) { |
|||
sylvan_deref(res1); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res2); |
|||
|
|||
BDD left = CALL(sylvan_exists, aLow, _v, 0); |
|||
if (left == sylvan_invalid) { |
|||
sylvan_deref(res1); |
|||
sylvan_deref(res2); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(left); |
|||
|
|||
BDD res1Inf = sylvan_ite(left, res1, sylvan_false); |
|||
if (res1Inf == sylvan_invalid) { |
|||
sylvan_deref(res1); |
|||
sylvan_deref(res2); |
|||
sylvan_deref(left); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res1Inf); |
|||
sylvan_deref(res1); |
|||
|
|||
BDD res2Inf = sylvan_ite(left, sylvan_false, res2); |
|||
if (res2Inf == sylvan_invalid) { |
|||
sylvan_deref(res2); |
|||
sylvan_deref(left); |
|||
sylvan_deref(res1Inf); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res2Inf); |
|||
sylvan_deref(res2); |
|||
sylvan_deref(left); |
|||
|
|||
assert(res1Inf != res2Inf); |
|||
BDD res = sylvan_ite(sylvan_ithvar(level), res2Inf, res1Inf); |
|||
if (res == sylvan_invalid) { |
|||
sylvan_deref(res1Inf); |
|||
sylvan_deref(res2Inf); |
|||
return sylvan_invalid; |
|||
} |
|||
|
|||
// cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); |
|||
// TODO: CACHING HERE |
|||
|
|||
sylvan_deref(res1Inf); |
|||
sylvan_deref(res2Inf); |
|||
|
|||
//printf("return properly computed result...\n"); |
|||
return res; |
|||
} else { /* if (level == vv) */ |
|||
BDD res1 = CALL(sylvan_existsRepresentative, aLow, variables, level); |
|||
if (res1 == sylvan_invalid){ |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res1); |
|||
|
|||
BDD res2 = CALL(sylvan_existsRepresentative, aHigh, variables, level); |
|||
if (res2 == sylvan_invalid) { |
|||
sylvan_deref(res1); |
|||
return sylvan_invalid; |
|||
} |
|||
sylvan_ref(res2); |
|||
|
|||
/* ITE takes care of possible complementation of res1 and of the |
|||
** case in which res1 == res2. */ |
|||
BDD res = sylvan_ite(sylvan_ithvar(level), res2, res1); |
|||
if (res == sylvan_invalid) { |
|||
sylvan_deref(res1); |
|||
sylvan_deref(res2); |
|||
return sylvan_invalid; |
|||
} |
|||
|
|||
sylvan_deref(res1); |
|||
sylvan_deref(res2); |
|||
|
|||
//printf("return of last case...\n"); |
|||
return res; |
|||
} |
|||
|
|||
// Prevent unused variable warning |
|||
(void)prev_level; |
|||
} |
|||
@ -1,3 +1,6 @@ |
|||
#define bdd_isnegated(dd) ((dd & sylvan_complement) ? 1 : 0) |
|||
#define bdd_regular(dd) (dd & ~sylvan_complement) |
|||
#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) |
|||
#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) |
|||
|
|||
TASK_DECL_3(BDD, sylvan_existsRepresentative, BDD, BDD, BDDVAR); |
|||
#define sylvan_existsRepresentative(a, vars) (CALL(sylvan_existsRepresentative, a, vars, 0)) |
|||
@ -1,3 +1,7 @@ |
|||
Mtbdd toDoubleMtbdd() const; |
|||
Mtbdd toInt64Mtbdd() const; |
|||
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
|
|||
Mtbdd toStormRationalFunctionMtbdd() const; |
|||
#endif
|
|||
Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; |
|||
Bdd ExistAbstractRepresentative(const BddSet& cube) const; |
|||
@ -0,0 +1,457 @@ |
|||
#include <sylvan_config.h> |
|||
|
|||
#include <assert.h> |
|||
#include <inttypes.h> |
|||
#include <math.h> |
|||
#include <stdint.h> |
|||
#include <stdio.h> |
|||
#include <stdlib.h> |
|||
#include <string.h> |
|||
|
|||
#include <sylvan.h> |
|||
#include <sylvan_common.h> |
|||
#include <sylvan_mtbdd_int.h> |
|||
#include <sylvan_storm_rational_function.h> |
|||
|
|||
#include <storm_function_wrapper.h> |
|||
|
|||
#undef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
|
|||
#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
int depth = 0; |
|||
|
|||
#define LOG_I(funcName) do { for (int i = 0; i < depth; ++i) { printf(" "); } ++depth; printf("Entering function " funcName "\n"); } while (0 != 0); |
|||
#define LOG_O(funcName) do { --depth; for (int i = 0; i < depth; ++i) { printf(" "); } printf("Leaving function " funcName "\n"); } while (0 != 0); |
|||
#else |
|||
#define LOG_I(funcName) |
|||
#define LOG_O(funcName) |
|||
#endif |
|||
|
|||
/** |
|||
* helper function for hash |
|||
*/ |
|||
#ifndef rotl64 |
|||
static inline uint64_t |
|||
rotl64(uint64_t x, int8_t r) |
|||
{ |
|||
return ((x<<r) | (x>>(64-r))); |
|||
} |
|||
#endif |
|||
|
|||
static uint64_t |
|||
sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) |
|||
{ |
|||
LOG_I("i-hash") |
|||
/* Hash the storm::RationalFunction in pointer v */ |
|||
|
|||
storm_rational_function_ptr x = (storm_rational_function_ptr)v; |
|||
|
|||
uint64_t hash = storm_rational_function_hash(x, seed); |
|||
|
|||
#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
printf("Hashing ptr %p with contents ", x); |
|||
print_storm_rational_function(x); |
|||
printf(" with seed %zu, hash = %zu\n", seed, hash); |
|||
#endif |
|||
|
|||
LOG_O("i-hash") |
|||
return hash; |
|||
} |
|||
|
|||
static int |
|||
sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) |
|||
{ |
|||
LOG_I("i-equals") |
|||
/* This function is called by the unique table when comparing a new |
|||
leaf with an existing leaf */ |
|||
storm_rational_function_ptr a = (storm_rational_function_ptr)(size_t)left; |
|||
storm_rational_function_ptr b = (storm_rational_function_ptr)(size_t)right; |
|||
|
|||
/* Just compare x and y */ |
|||
int result = storm_rational_function_equals(a, b); |
|||
|
|||
LOG_O("i-equals") |
|||
return result; |
|||
} |
|||
|
|||
static void |
|||
sylvan_storm_rational_function_create(uint64_t *val) |
|||
{ |
|||
LOG_I("i-create") |
|||
|
|||
#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
void* tmp = (void*)*val; |
|||
printf("sylvan_storm_rational_function_create(ptr = %p, value = ", tmp); |
|||
print_storm_rational_function(*((storm_rational_function_ptr*)(size_t)val)); |
|||
printf(")\n"); |
|||
#endif |
|||
|
|||
/* This function is called by the unique table when a leaf does not yet exist. |
|||
We make a copy, which will be stored in the hash table. */ |
|||
storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val; |
|||
storm_rational_function_init(x); |
|||
|
|||
#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
tmp = (void*)*val; |
|||
printf("sylvan_storm_rational_function_create_2(ptr = %p)\n", tmp); |
|||
#endif |
|||
|
|||
LOG_O("i-create") |
|||
} |
|||
|
|||
static void |
|||
sylvan_storm_rational_function_destroy(uint64_t val) |
|||
{ |
|||
LOG_I("i-destroy") |
|||
/* This function is called by the unique table |
|||
when a leaf is removed during garbage collection. */ |
|||
storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val; |
|||
storm_rational_function_destroy(x); |
|||
LOG_O("i-destroy") |
|||
} |
|||
|
|||
static uint32_t sylvan_storm_rational_function_type; |
|||
static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS; |
|||
|
|||
/** |
|||
* Initialize storm::RationalFunction custom leaves |
|||
*/ |
|||
void |
|||
sylvan_storm_rational_function_init() |
|||
{ |
|||
/* Register custom leaf 3 */ |
|||
sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy); |
|||
|
|||
if (SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID != sylvan_storm_rational_function_type) { |
|||
printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling StoRM!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type); |
|||
assert(0); |
|||
} |
|||
|
|||
CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid(); |
|||
} |
|||
|
|||
uint32_t sylvan_storm_rational_function_get_type() { |
|||
return sylvan_storm_rational_function_type; |
|||
} |
|||
|
|||
/** |
|||
* Create storm::RationalFunction leaf |
|||
*/ |
|||
MTBDD |
|||
mtbdd_storm_rational_function(storm_rational_function_ptr val) |
|||
{ |
|||
LOG_I("i-mtbdd_") |
|||
uint64_t terminalValue = (uint64_t)val; |
|||
|
|||
#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG |
|||
printf("mtbdd_storm_rational_function(ptr = %p, value = ", val); |
|||
print_storm_rational_function(val); |
|||
printf(")\n"); |
|||
#endif |
|||
|
|||
MTBDD result = mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue); |
|||
|
|||
LOG_O("i-mtbdd_") |
|||
return result; |
|||
} |
|||
|
|||
/** |
|||
* Converts a BDD to a MTBDD with storm::RationalFunction leaves |
|||
*/ |
|||
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) { |
|||
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) { |
|||
MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_one()); |
|||
LOG_O("task_impl_2 to_srf - ONE") |
|||
return result; |
|||
} |
|||
|
|||
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). |
|||
(void)v; |
|||
|
|||
LOG_O("task_impl_2 to_srf - INVALID") |
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) |
|||
{ |
|||
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0); |
|||
} |
|||
|
|||
/** |
|||
* Operation "plus" for two storm::RationalFunction MTBDDs |
|||
* Interpret partial function as "0" |
|||
*/ |
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb) |
|||
{ |
|||
LOG_I("task_impl_2 op_plus") |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false) return b; |
|||
if (b == mtbdd_false) return a; |
|||
|
|||
/* If both leaves, compute plus */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); |
|||
storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); |
|||
|
|||
storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_function(mres); |
|||
|
|||
// TODO: Delete mres? |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so swap a,b for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
/** |
|||
* Operation "minus" for two storm::RationalFunction MTBDDs |
|||
* Interpret partial function as "0" |
|||
*/ |
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb) |
|||
{ |
|||
LOG_I("task_impl_2 op_minus") |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b); |
|||
if (b == mtbdd_false) return a; |
|||
|
|||
/* If both leaves, compute plus */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); |
|||
storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); |
|||
|
|||
storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_function(mres); |
|||
|
|||
// TODO: Delete mres? |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
/** |
|||
* Operation "times" for two storm::RationalFunction MTBDDs. |
|||
* One of the parameters can be a BDD, then it is interpreted as a filter. |
|||
* For partial functions, domain is intersection |
|||
*/ |
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb) |
|||
{ |
|||
LOG_I("task_impl_2 op_times") |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If one of Boolean, interpret as filter */ |
|||
if (a == mtbdd_true) return b; |
|||
if (b == mtbdd_true) return a; |
|||
|
|||
/* Handle multiplication of leaves */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); |
|||
storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); |
|||
|
|||
storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_function(mres); |
|||
|
|||
// TODO: Delete mres? |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so make "a" the lowest for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
/** |
|||
* Operation "divide" for two storm::RationalFunction MTBDDs. |
|||
* For partial functions, domain is intersection |
|||
*/ |
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb) |
|||
{ |
|||
LOG_I("task_impl_2 op_divide") |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Handle division of leaves */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); |
|||
storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); |
|||
|
|||
storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_function(mres); |
|||
|
|||
// TODO: Delete mres? |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
/** |
|||
* The abstraction operators are called in either of two ways: |
|||
* - with k=0, then just calculate "a op b" |
|||
* - with k<>0, then just calculate "a := a op a", k times |
|||
*/ |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) |
|||
{ |
|||
LOG_I("task_impl_3 abstract_op_plus") |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_plus)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k) |
|||
{ |
|||
LOG_I("task_impl_3 abstract_op_times") |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_function_op_times)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
/** |
|||
* Operation "neg" for one storm::RationalFunction MTBDD |
|||
*/ |
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) |
|||
{ |
|||
LOG_I("task_impl_2 op_neg") |
|||
/* Handle partial functions */ |
|||
if (dd == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Compute result for leaf */ |
|||
if (mtbdd_isleaf(dd)) { |
|||
storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); |
|||
|
|||
storm_rational_function_ptr mres = storm_rational_function_negate(mdd); |
|||
MTBDD res = mtbdd_storm_rational_function(mres); |
|||
|
|||
// TODO: Delete mres? |
|||
return res; |
|||
} |
|||
|
|||
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; |
|||
} |
|||
@ -0,0 +1,113 @@ |
|||
/** |
|||
* This is an implementation of storm::RationalFunction custom leaves of MTBDDs |
|||
*/ |
|||
|
|||
#ifndef SYLVAN_STORM_RATIONAL_FUNCTION_H |
|||
#define SYLVAN_STORM_RATIONAL_FUNCTION_H |
|||
|
|||
#include <sylvan.h> |
|||
#include <storm_function_wrapper.h> |
|||
|
|||
#define SYLVAN_HAVE_CARL 1 |
|||
|
|||
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) |
|||
|
|||
#define SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID (3) |
|||
|
|||
#ifdef __cplusplus |
|||
extern "C" { |
|||
#endif /* __cplusplus */ |
|||
|
|||
/** |
|||
* Initialize storm::RationalFunction custom leaves |
|||
*/ |
|||
void sylvan_storm_rational_function_init(); |
|||
|
|||
/** |
|||
* Returns the identifier necessary to use these custom leaves. |
|||
*/ |
|||
uint32_t sylvan_storm_rational_function_get_type(); |
|||
|
|||
/** |
|||
* Create storm::RationalFunction leaf |
|||
*/ |
|||
MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val); |
|||
|
|||
/** |
|||
* Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise; |
|||
*/ |
|||
TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t) |
|||
TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD) |
|||
#define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd) |
|||
|
|||
/** |
|||
* Operation "plus" for two storm::RationalFunction MTBDDs |
|||
*/ |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*) |
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int) |
|||
|
|||
/** |
|||
* Operation "minus" for two storm::RationalFunction MTBDDs |
|||
*/ |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*) |
|||
|
|||
/** |
|||
* Operation "times" for two storm::RationalFunction MTBDDs |
|||
*/ |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*) |
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int) |
|||
|
|||
/** |
|||
* Operation "divide" for two storm::RationalFunction MTBDDs |
|||
*/ |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*) |
|||
|
|||
/** |
|||
* Operation "negate" for one storm::RationalFunction MTBDD |
|||
*/ |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) |
|||
|
|||
/** |
|||
* Compute a + b |
|||
*/ |
|||
#define sylvan_storm_rational_function_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)) |
|||
|
|||
/** |
|||
* Compute a - b |
|||
*/ |
|||
#define sylvan_storm_rational_function_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_minus)) |
|||
|
|||
/** |
|||
* Compute a * b |
|||
*/ |
|||
#define sylvan_storm_rational_function_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)) |
|||
|
|||
/** |
|||
* Compute a / b |
|||
*/ |
|||
#define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide)) |
|||
|
|||
/** |
|||
* Compute -a |
|||
*/ |
|||
#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) |
|||
|
|||
/** |
|||
* Abstract the variables in <v> from <a> by taking the sum of all values |
|||
*/ |
|||
#define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) |
|||
|
|||
#ifdef __cplusplus |
|||
} |
|||
#endif /* __cplusplus */ |
|||
|
|||
#endif // SYLVAN_HAVE_CARL |
|||
|
|||
#endif // SYLVAN_STORM_RATIONAL_FUNCTION_H |
|||
@ -1,151 +1,168 @@ |
|||
#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|||
#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|||
|
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/storage/dd/DdType.h" |
|||
#include "src/storage/dd/InternalDdManager.h" |
|||
|
|||
#include "src/storage/dd/sylvan/InternalSylvanBdd.h" |
|||
#include "src/storage/dd/sylvan/InternalSylvanAdd.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<DdType LibraryType, typename ValueType> |
|||
class InternalAdd; |
|||
|
|||
template<DdType LibraryType> |
|||
class InternalBdd; |
|||
|
|||
template<> |
|||
class InternalDdManager<DdType::Sylvan> { |
|||
public: |
|||
friend class InternalBdd<DdType::Sylvan>; |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
friend class InternalAdd; |
|||
|
|||
/*! |
|||
* Creates a new internal manager for Sylvan DDs. |
|||
*/ |
|||
InternalDdManager(); |
|||
|
|||
/*! |
|||
* Destroys the internal manager. |
|||
*/ |
|||
~InternalDdManager(); |
|||
|
|||
/*! |
|||
* Retrieves a BDD representing the constant one function. |
|||
* |
|||
* @return A BDD representing the constant one function. |
|||
*/ |
|||
InternalBdd<DdType::Sylvan> getBddOne() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant one function. |
|||
* |
|||
* @return An ADD representing the constant one function. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getAddOne() const; |
|||
|
|||
/*! |
|||
* Retrieves a BDD representing the constant zero function. |
|||
* |
|||
* @return A BDD representing the constant zero function. |
|||
*/ |
|||
InternalBdd<DdType::Sylvan> getBddZero() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant zero function. |
|||
* |
|||
* @return An ADD representing the constant zero function. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getAddZero() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant function with the given value. |
|||
* |
|||
* @return An ADD representing the constant function with the given value. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const; |
|||
|
|||
/*! |
|||
* Creates a new pair of DD variables and returns the two cubes as a result. |
|||
* |
|||
* @param position An optional position at which to insert the new variable pair. This may only be given, if |
|||
* the manager supports ordered insertion. |
|||
* @return The two cubes belonging to the DD variables. |
|||
*/ |
|||
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair(boost::optional<uint_fast64_t> const& position = boost::none); |
|||
|
|||
/*! |
|||
* Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at |
|||
* positions between already existing variables. |
|||
* |
|||
* @return True iff the manager supports ordered insertion. |
|||
*/ |
|||
bool supportsOrderedInsertion() const; |
|||
|
|||
/*! |
|||
* Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. |
|||
* |
|||
* @param value If set to true, dynamic reordering is allowed and forbidden otherwise. |
|||
*/ |
|||
void allowDynamicReordering(bool value); |
|||
|
|||
/*! |
|||
* Retrieves whether dynamic reordering is currently allowed. |
|||
* |
|||
* @return True iff dynamic reordering is currently allowed. |
|||
*/ |
|||
bool isDynamicReorderingAllowed() const; |
|||
|
|||
/*! |
|||
* Triggers a reordering of the DDs managed by this manager. |
|||
*/ |
|||
void triggerReordering(); |
|||
|
|||
/*! |
|||
* Retrieves the number of DD variables managed by this manager. |
|||
* |
|||
* @return The number of managed variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfDdVariables() const; |
|||
|
|||
private: |
|||
// A counter for the number of instances of this class. This is used to determine when to initialize and |
|||
// quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a |
|||
// 'global' manager. |
|||
static uint_fast64_t numberOfInstances; |
|||
|
|||
// The index of the next free variable index. This needs to be shared across all instances since the sylvan |
|||
// manager is implicitly 'global'. |
|||
static uint_fast64_t nextFreeVariableIndex; |
|||
}; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
|||
|
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ |
|||
#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|||
#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|||
|
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/storage/dd/DdType.h" |
|||
#include "src/storage/dd/InternalDdManager.h" |
|||
|
|||
#include "src/storage/dd/sylvan/InternalSylvanBdd.h" |
|||
#include "src/storage/dd/sylvan/InternalSylvanAdd.h" |
|||
|
|||
#include "src/adapters/CarlAdapter.h" |
|||
#include "storm-config.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<DdType LibraryType, typename ValueType> |
|||
class InternalAdd; |
|||
|
|||
template<DdType LibraryType> |
|||
class InternalBdd; |
|||
|
|||
template<> |
|||
class InternalDdManager<DdType::Sylvan> { |
|||
public: |
|||
friend class InternalBdd<DdType::Sylvan>; |
|||
|
|||
template<DdType LibraryType, typename ValueType> |
|||
friend class InternalAdd; |
|||
|
|||
/*! |
|||
* Creates a new internal manager for Sylvan DDs. |
|||
*/ |
|||
InternalDdManager(); |
|||
|
|||
/*! |
|||
* Destroys the internal manager. |
|||
*/ |
|||
~InternalDdManager(); |
|||
|
|||
/*! |
|||
* Retrieves a BDD representing the constant one function. |
|||
* |
|||
* @return A BDD representing the constant one function. |
|||
*/ |
|||
InternalBdd<DdType::Sylvan> getBddOne() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant one function. |
|||
* |
|||
* @return An ADD representing the constant one function. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getAddOne() const; |
|||
|
|||
/*! |
|||
* Retrieves a BDD representing the constant zero function. |
|||
* |
|||
* @return A BDD representing the constant zero function. |
|||
*/ |
|||
InternalBdd<DdType::Sylvan> getBddZero() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant zero function. |
|||
* |
|||
* @return An ADD representing the constant zero function. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getAddZero() const; |
|||
|
|||
/*! |
|||
* Retrieves an ADD representing the constant function with the given value. |
|||
* |
|||
* @return An ADD representing the constant function with the given value. |
|||
*/ |
|||
template<typename ValueType> |
|||
InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const; |
|||
|
|||
/*! |
|||
* Creates a new pair of DD variables and returns the two cubes as a result. |
|||
* |
|||
* @param position An optional position at which to insert the new variable pair. This may only be given, if |
|||
* the manager supports ordered insertion. |
|||
* @return The two cubes belonging to the DD variables. |
|||
*/ |
|||
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair(boost::optional<uint_fast64_t> const& position = boost::none); |
|||
|
|||
/*! |
|||
* Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at |
|||
* positions between already existing variables. |
|||
* |
|||
* @return True iff the manager supports ordered insertion. |
|||
*/ |
|||
bool supportsOrderedInsertion() const; |
|||
|
|||
/*! |
|||
* Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. |
|||
* |
|||
* @param value If set to true, dynamic reordering is allowed and forbidden otherwise. |
|||
*/ |
|||
void allowDynamicReordering(bool value); |
|||
|
|||
/*! |
|||
* Retrieves whether dynamic reordering is currently allowed. |
|||
* |
|||
* @return True iff dynamic reordering is currently allowed. |
|||
*/ |
|||
bool isDynamicReorderingAllowed() const; |
|||
|
|||
/*! |
|||
* Triggers a reordering of the DDs managed by this manager. |
|||
*/ |
|||
void triggerReordering(); |
|||
|
|||
/*! |
|||
* Retrieves the number of DD variables managed by this manager. |
|||
* |
|||
* @return The number of managed variables. |
|||
*/ |
|||
uint_fast64_t getNumberOfDdVariables() const; |
|||
|
|||
private: |
|||
// A counter for the number of instances of this class. This is used to determine when to initialize and |
|||
// quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a |
|||
// 'global' manager. |
|||
static uint_fast64_t numberOfInstances; |
|||
|
|||
// The index of the next free variable index. This needs to be shared across all instances since the sylvan |
|||
// manager is implicitly 'global'. |
|||
static uint_fast64_t nextFreeVariableIndex; |
|||
}; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|||
|
|||
#ifdef STORM_HAVE_CARL |
|||
template<> |
|||
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|||
#endif |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|||
|
|||
#ifdef STORM_HAVE_CARL |
|||
template<> |
|||
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|||
#endif |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
|||
|
|||
template<> |
|||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
|||
|
|||
#ifdef STORM_HAVE_CARL |
|||
template<> |
|||
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const; |
|||
#endif |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ |
|||
@ -1,19 +1,20 @@ |
|||
#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|||
#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|||
|
|||
#pragma clang diagnostic push |
|||
#pragma clang diagnostic ignored "-Wextra-semi" |
|||
#pragma clang diagnostic ignored "-Wzero-length-array" |
|||
#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" |
|||
#pragma clang diagnostic ignored "-Wdeprecated-register" |
|||
#pragma clang diagnostic ignored "-Wc99-extensions" |
|||
#pragma clang diagnostic ignored "-Wunknown-pragmas" |
|||
#pragma GCC diagnostic push |
|||
#pragma GCC diagnostic ignored "-Wpedantic" |
|||
|
|||
#include "sylvan_obj.hpp" |
|||
|
|||
#pragma GCC diagnostic pop |
|||
#pragma clang diagnostic pop |
|||
|
|||
#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|||
#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|||
|
|||
#pragma clang diagnostic push |
|||
#pragma clang diagnostic ignored "-Wextra-semi" |
|||
#pragma clang diagnostic ignored "-Wzero-length-array" |
|||
#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" |
|||
#pragma clang diagnostic ignored "-Wdeprecated-register" |
|||
#pragma clang diagnostic ignored "-Wc99-extensions" |
|||
#pragma clang diagnostic ignored "-Wunknown-pragmas" |
|||
#pragma GCC diagnostic push |
|||
#pragma GCC diagnostic ignored "-Wpedantic" |
|||
|
|||
#include "sylvan_obj.hpp" |
|||
#include "sylvan_storm_rational_function.h" |
|||
|
|||
#pragma GCC diagnostic pop |
|||
#pragma clang diagnostic pop |
|||
|
|||
#endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue