Author: karstenwolf
Date: Sun Jun 1 10:50:00 2014
New Revision: 9482
URL: http://svn.gna.org/viewcvs/service-tech?rev=9482&view=rev
Log:
Folgendes scheint zu funktionieren:
- EF DEADLOCK
- AG DEADLOCK
- AG NOT DEADLOCK ... wird alles auf initial oder deadlocks reduziert
- AG ( DEADLOCK -> hl.1 > 0) ... wird auf statepredicate reduziert.
hab aber noch nicht allzu intensiv getestet...
Modified:
trunk/lola2/src/Frontend/Parser/formula_rewrite.k
trunk/lola2/src/Frontend/Parser/formula_unparse.k
Modified: trunk/lola2/src/Frontend/Parser/formula_rewrite.k
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Frontend/Parser/formula_rewrite.k?rev=9482&r1=9481&r2=9482&view=diff
==============================================================================
--- trunk/lola2/src/Frontend/Parser/formula_rewrite.k (original)
+++ trunk/lola2/src/Frontend/Parser/formula_rewrite.k Sun Jun 1 10:50:00 2014
@@ -743,6 +743,24 @@
// NOT (x OR y) -> (NOT x AND NOT y)
Negation(Disjunction(x, y)) -> <simpleneg: Conjunction(Negation(x),
Negation(y))>;
+// NOT TRUE -> FALSE
+Negation(AtomicProposition(True())) -> <simpleneg: AtomicProposition(False())>;
+
+// NOT FALSE -> TRUE
+Negation(AtomicProposition(False())) -> <simpleneg: AtomicProposition(True())>;
+
+// NOT deadlock -> nodeadlock
+Negation(AtomicProposition(Deadlock())) -> <simpleneg:
AtomicProposition(NoDeadlock())>;
+
+// NOT nodeadlock -> deadlock
+Negation(AtomicProposition(NoDeadlock())) -> <simpleneg:
AtomicProposition(Deadlock())>;
+
+// NOT (p > n) -> p <= n
+Negation(AtomicProposition(GreaterAtomicProposition(p,n))) -> <simpleneg:
AtomicProposition(LessEqualAtomicProposition(p, n))>;
+
+// NOT (p <= n) -> p > n
+Negation(AtomicProposition(LessEqualAtomicProposition(p,n))) -> <simpleneg:
AtomicProposition(GreaterAtomicProposition(p, n))>;
+
%rview booleanlists;
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=9482&r1=9481&r2=9482&view=diff
==============================================================================
--- trunk/lola2/src/Frontend/Parser/formula_unparse.k (original)
+++ trunk/lola2/src/Frontend/Parser/formula_unparse.k Sun Jun 1 10:50:00 2014
@@ -111,7 +111,7 @@
False() -> [out: "FALSE"];
Initial() -> [out: "INITIAL"];
Deadlock() -> [out: "DEADLOCK"];
-NoDeadlock() -> [out: "(! DEADLOCK)"];
+NoDeadlock() -> [out: "! DEADLOCK"];
Fireable(x) -> [out: "FIREABLE(" { kc_printer(kc_t(Net::Name[TR][x->value]),
kc_current_view); } ")"];
Node(x) -> [out: { kc_printer(kc_t(Net::Name[PL][x->value]), kc_current_view);
}];
--
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.
