~verifytapn/verifytapn/1.0

« back to all changes in this revision

Viewing changes to src/main.cpp

Committer: Lasse Jacobsen
Date: 2010-11-25 13:44:42 UTC
Revision ID: lassejac@lassejac-laptop-20101125134442-65r093ij17ylh410

- added experimental feature for using either global of local max constants
for extrapolation

files modified:
src/Core/VerificationOptions.cpp

src/Core/VerificationOptions.hpp

src/Verification/SearchStrategy.cpp

src/main.cpp

Show diffs side-by-side

added added

removed removed

src/main.cpp

using namespace VerifyTAPN::TAPN;

using namespace boost;

void test()

{

dbm::dbm_t dbm(3);

dbm.setInit();

dbm.constrain(0,1, dbm_bound2raw(-1, dbm_WEAK));

dbm.constrain(1,0,dbm_bound2raw(3,dbm_WEAK));

dbm.constrain(0,2,dbm_bound2raw(-1,dbm_WEAK));

dbm.constrain(2,0,dbm_bound2raw(5,dbm_WEAK));

dbm.constrain(1,2,dbm_bound2raw(2,dbm_WEAK));

dbm.constrain(2,1,dbm_bound2raw(2, dbm_WEAK));

int max[] = { 3,-dbm_INFINITY,3 };

std::cout << "dbm: \n";

std::cout << dbm << "\n\n";

dbm::dbm_t dbm2(3);

dbm2.setInit();

dbm2.constrain(0,1, dbm_bound2raw(-2, dbm_WEAK));

dbm2.constrain(1,0,dbm_bound2raw(3,dbm_WEAK));

dbm2.constrain(0,2,dbm_bound2raw(-1,dbm_WEAK));

dbm2.constrain(2,0,dbm_bound2raw(4,dbm_WEAK));

dbm2.constrain(1,2,dbm_bound2raw(2,dbm_WEAK));

dbm2.constrain(2,1,dbm_bound2raw(2, dbm_WEAK));

std::cout << "dbm2: \n";

std::cout << dbm2 << "\n\n";

relation_t relation = dbm2.relation(dbm);

std::cout << "relation:\n";

std::cout << "dbm2 <subset eq> dbm: " << ((relation & base_SUBSET) != 0 ? "true" : "false") << "\n";

dbm2.extrapolateMaxBounds(max);

std::cout << "dbm2 inactive:\n";

std::cout << dbm2 << "\n";

relation = dbm2.relation(dbm);

std::cout << "relation:\n";

std::cout << "dbm2 <subset eq> dbm: " << ((relation & base_SUBSET) != 0 ? "true" : "false") << "\n";

}

int main(int argc, char* argv[]) {

//test();

VerificationOptions options = VerificationOptions::ParseVerificationOptions(argc, argv);

TAPNXmlParser modelParser;

Older »