Author: vm069
Date: Mon May 26 14:55:42 2014
New Revision: 9458
URL: http://svn.gna.org/viewcvs/service-tech?rev=9458&view=rev
Log:
included new formulatypes
Modified:
trunk/lola2/src/Core/Dimensions.h
trunk/lola2/src/Frontend/Parser/formula_unparse.k
trunk/lola2/src/Planning/Task.cc
Modified: trunk/lola2/src/Core/Dimensions.h
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Core/Dimensions.h?rev=9458&r1=9457&r2=9458&view=diff
==============================================================================
--- trunk/lola2/src/Core/Dimensions.h (original)
+++ trunk/lola2/src/Core/Dimensions.h Mon May 26 14:55:42 2014
@@ -122,7 +122,9 @@
FORMULA_LTL = 7, ///< LTL formulae
FORMULA_CTL = 8, ///< CTL formulae
FORMULA_MODELCHECKING = 9, ///< CTL* formulae
- FORMULA_DEADLOCK = 10 ///< deadlock
+ FORMULA_DEADLOCK = 10, ///< deadlock
+ FORMULA_AGAF = 11, ///< AGAF
+ FORMULA_EFAGEF = 12 ///< EFAGEF
} formula_t;
/// three-valued logic
Modified: trunk/lola2/src/Frontend/Parser/formula_unparse.k
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Frontend/Parser/formula_unparse.k?rev=9458&r1=9457&r2=9458&view=diff
==============================================================================
--- trunk/lola2/src/Frontend/Parser/formula_unparse.k (original)
+++ trunk/lola2/src/Frontend/Parser/formula_unparse.k Mon May 26 14:55:42 2014
@@ -155,6 +155,9 @@
{ f->type = FORMULA_INVARIANT; }
AllPath(Always(ExPath(Eventually(y)))) provided (not
y->containsTemporal) :
{ f->type = FORMULA_LIVENESS; }
+ AllPath(Always(AllPath(Eventually(y)))) provided (not
y->containsTemporal) :
+ { f->type = FORMULA_AGAF; }
+ ExPath(Eventually(AllPath(Always(ExPath(Eventually(y)))))) provided
(not y->containsTemporal) : { f->type = FORMULA_EFAGEF; }
Always(Eventually(y)) provided (not y->containsTemporal) :
{ f->type = FORMULA_FAIRNESS; }
Eventually(Always(y)) provided (not y->containsTemporal) :
Modified: trunk/lola2/src/Planning/Task.cc
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Planning/Task.cc?rev=9458&r1=9457&r2=9458&view=diff
==============================================================================
--- trunk/lola2/src/Planning/Task.cc (original)
+++ trunk/lola2/src/Planning/Task.cc Mon May 26 14:55:42 2014
@@ -342,16 +342,11 @@
break;
}
- //TODO remove the condition when TSCC is included to the frontend
- // its only for debug/testing purposes
- if (!RT::args.tscc_flag)
- {
- formulaType = FORMULA_CTL;
- }
- else
- {
- RT::rep->status("liveness not yet implemented, converting to
CTL...");
- }
+ //formulaType = FORMULA_CTL;
+ //RT::rep->status("liveness not yet implemented, converting to
CTL...");
+ break;
+ case (FORMULA_AGAF):
+ RT::rep->status("checking AGAF");
break;
case (FORMULA_FAIRNESS):
RT::rep->status("checking fairness");
@@ -392,7 +387,7 @@
RT::rep->status("processing formula");
// simplify CTL formula to fewer operators
- if (formulaType == FORMULA_CTL && !RT::args.tscc_flag)
+ if (formulaType == FORMULA_CTL)
{
// replace path quantor+temporal operator by dedicated CTL operator
TheFormula = TheFormula->rewrite(kc::ctloperators);
@@ -414,6 +409,14 @@
case FORMULA_REACHABLE:
case FORMULA_INVARIANT:
case FORMULA_INITIAL:
+ case FORMULA_AGAF:
+ {
+ if(RT::args.tscc_flag)
+ {
+ TheFormula = TheFormula->rewrite(kc::booleanlists);
+ }
+ break;
+ }
case FORMULA_LIVENESS: // currently only for cover graphs!
{
TheFormula = TheFormula->rewrite(kc::booleanlists);
@@ -470,10 +473,8 @@
spFormula = result;
break;
}
-
- case FORMULA_CTL:
- {
- if(RT::args.tscc_flag){
+ case FORMULA_AGAF:
+ {
TheFormula->unparse(myprinter, kc::internal);
StatePredicate *result = TheFormula->formula;
@@ -483,13 +484,14 @@
RT::data["analysis"]["formula"]["atomic_propositions"] =
static_cast<int>(result->countAtomic());
spFormula = result;
- }else{
-
- TheFormula->unparse(myprinter, kc::ctl);
- ctlFormula = TheFormula->ctl_formula;
-
- assert(ctlFormula);
- }
+ }
+
+ case FORMULA_CTL:
+ {
+ TheFormula->unparse(myprinter, kc::ctl);
+ ctlFormula = TheFormula->ctl_formula;
+
+ assert(ctlFormula);
break;
}
@@ -888,11 +890,11 @@
fl = new Firelist();
if (RT::args.tscc_flag)
{
- if(formulaType==FORMULA_LIVENESS)
+ if(formulaType == FORMULA_LIVENESS)
{
tsccExploration = new TSCCExplorationAGEF();
}
- else
+ else if (formulaType == FORMULA_AGAF)
{
tsccExploration = new TSCCExplorationAGAF();
}
--
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.
