Author: vm069
Date: Tue May 27 14:14:34 2014
New Revision: 9470
URL: http://svn.gna.org/viewcvs/service-tech?rev=9470&view=rev
Log:
implemented AGAF, repaired AGEF,modified tests
* the implementation of AGAF is now completed
* AGEF had a bug -> fixed
* modified the testcases to match the correct behavior
Modified:
trunk/lola2/src/Exploration/FirelistStubbornTscc.cc
trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc
trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc
trunk/lola2/src/Planning/Task.cc
trunk/lola2/tests/testsuite.at
Modified: trunk/lola2/src/Exploration/FirelistStubbornTscc.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/FirelistStubbornTscc.cc?rev=9470&r1=9469&r2=9470&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/FirelistStubbornTscc.cc (original)
+++ trunk/lola2/src/Exploration/FirelistStubbornTscc.cc Tue May 27 14:14:34 2014
@@ -24,7 +24,6 @@
sp =(StatePredicateProperty *) simpleproperty;
dfsStack = new index_t[Net::Card[TR]];
onStack = new bool[Net::Card[TR]]();
- fprintf(stderr,"created FirelistStubbornTscc\n");
}
FirelistStubbornTscc::~FirelistStubbornTscc()
Modified: trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc?rev=9470&r1=9469&r2=9470&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc (original)
+++ trunk/lola2/src/Exploration/TSCCExplorationAGAF.cc Tue May 27 14:14:34 2014
@@ -132,18 +132,19 @@
if(getDFS( (statenumber_t *) stackentry.payload) ==
stackentry.lowlink && highest_lowlink<stackentry.lowlink)
{
- //valid for agef :)
- if(lasttrue >= stackentry.lowlink)
+ //valid for agaf :)
+ if(lasttrue >= stackentry.lowlink )
{
//for the current tscc "add" one more true
//just for clarification of the code...
- result = result&true;
+ result = result and true;
}
- else{
- //there is a tscc in which the property is not true
- //then we can exit
- return false;
+ else if (lastfalse >= stackentry.lowlink)
+ {
+ result = result and false;
+ return result;
}
+
//update the highest lowlink to the current
highest_lowlink = stackentry.lowlink;
}
Modified: trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc?rev=9470&r1=9469&r2=9470&view=diff
==============================================================================
--- trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc (original)
+++ trunk/lola2/src/Exploration/TSCCExplorationAGEF.cc Tue May 27 14:14:34 2014
@@ -38,7 +38,6 @@
//last dfs where property was true
index_t lasttrue = 0;
- index_t lastfalse = 0;
//initialise dfsnumber,lowlink and highest_lowlink
statenumber_t currentDFSNumber = 0;
@@ -97,10 +96,6 @@
{
lasttrue = currentDFSNumber;
}
- else
- {
- lastfalse = currentDFSNumber;
- }
//update enabled transitions
Transition::updateEnabled(ns, currentFirelist[currentEntry]);
@@ -135,7 +130,7 @@
{
//for the current tscc "add" one more true
//just for clarification of the code...
- result = result&true;
+ return true;
}
else{
//there is a tscc in which the property is not true
Modified: trunk/lola2/src/Planning/Task.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Planning/Task.cc?rev=9470&r1=9469&r2=9470&view=diff
==============================================================================
--- trunk/lola2/src/Planning/Task.cc (original)
+++ trunk/lola2/src/Planning/Task.cc Tue May 27 14:14:34 2014
@@ -413,23 +413,13 @@
case FORMULA_INVARIANT:
case FORMULA_INITIAL:
case FORMULA_AGAF:
- {
- if(RT::args.tscc_flag)
- {
- TheFormula = TheFormula->rewrite(kc::booleanlists);
- }
- break;
- }
+ case FORMULA_EFAGEF:
case FORMULA_LIVENESS: // currently only for cover graphs!
{
TheFormula = TheFormula->rewrite(kc::booleanlists);
break;
}
default:
- if(RT::args.tscc_flag)
- {
- TheFormula = TheFormula->rewrite(kc::booleanlists);
- }
break;
}
@@ -464,6 +454,8 @@
case FORMULA_REACHABLE:
case FORMULA_INVARIANT:
case FORMULA_INITIAL:
+ case FORMULA_AGAF:
+ case FORMULA_EFAGEF:
case FORMULA_LIVENESS: // currently only for cover graphs!
{
// copy restructured formula into internal data structures
@@ -478,19 +470,6 @@
spFormula = result;
break;
}
- case FORMULA_AGAF:
- {
- TheFormula->unparse(myprinter, kc::internal);
- StatePredicate *result = TheFormula->formula;
-
- assert(result);
- RT::rep->status("processed formula with %d atomic propositions",
- result->countAtomic());
- RT::data["analysis"]["formula"]["atomic_propositions"] =
static_cast<int>(result->countAtomic());
-
- spFormula = result;
- }
-
case FORMULA_CTL:
{
TheFormula->unparse(myprinter, kc::ctl);
@@ -902,6 +881,10 @@
else if (formulaType == FORMULA_AGAF)
{
tsccExploration = new TSCCExplorationAGAF();
+ }
+ else if(formulaType == FORMULA_EFAGEF )
+ {
+ tsccExploration = new TSCCExplorationEFAGEF();
}
assert(spFormula);
p = new StatePredicateProperty(spFormula);
Modified: trunk/lola2/tests/testsuite.at
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/tests/testsuite.at?rev=9470&r1=9469&r2=9470&view=diff
==============================================================================
--- trunk/lola2/tests/testsuite.at (original)
+++ trunk/lola2/tests/testsuite.at Tue May 27 14:14:34 2014
@@ -2292,14 +2292,14 @@
AT_SETUP([liveness tscc(negative formula)])
AT_CHECK([cp TESTFILES/tscc.lola .])
AT_CHECK([LOLA tscc.lola --tscc --formula='"AGEF p5 > 0"' --check=full
],0,stdout,stderr)
-AT_CHECK([GREP -q "lola: result: no" stderr])
+AT_CHECK([GREP -q "lola: result: yes" stderr])
AT_KEYWORDS(tscc)
AT_CLEANUP
AT_SETUP([liveness tscc(ResAllocation (mcc 2014))])
AT_CHECK([cp TESTFILES/ResAllocation-PT-R003C002.lola
TESTFILES/ResAllocation-PT-R003C002-CTLCardinality-1.task .])
AT_CHECK([LOLA ResAllocation-PT-R003C002.lola --tscc
--formula=ResAllocation-PT-R003C002-CTLCardinality-1.task --check=full
],0,stdout,stderr)
-AT_CHECK([GREP -q "lola: result: no" stderr])
+AT_CHECK([GREP -q "lola: result: yes" stderr])
AT_KEYWORDS(tscc)
AT_CLEANUP
--
You received this e-mail, because you subscribed the mailing list
"service-tech-commits" which will forward you any e-mail addressed to
[email protected]. If you want to unsubscribe or make any changes to
your subscription, please go to
https://mail.gna.org/listinfo/service-tech-commits.
