Commit 0f48be2f authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

Was a copy paste mistake. Fixed it.



Issue-Ref: 3610
Signed-off-by: Sudeep Kanav's avatarSudeep Kanav <kanav@fortiss.org>
parent 1cbdbd68
AnalysisConstraintsUtils.java 1fe976ae3a57682ace37c347bd4b004f04b7c007 GREEN
CounterExampleUtils.java 8baec067cc6fa19eca36d022c210fdfa20e3be0f GREEN
SpecificationsFactory.java 5f9d03c8dbd052f50de944c7eb988eabc53c089a GREEN
SpecificationsFactory.java f5c6b78a3c837505030335cd0b05b2d37c6bb610 YELLOW
TLSpecificationUtils.java 205587b731e8b0695fe2bc59bb0222ef4d0c50a2 GREEN
Z3SpecificationUtils.java 47b2e48d9f9d8c311f762b979bb5050560a506bb GREEN
......@@ -58,7 +58,7 @@ public class SpecificationsFactory {
/** Creates the LTLSPEC <>R -> (!P U R) */
public static IExpressionTerm absenceBeforeLTL(IExpressionTerm p, IExpressionTerm r) {
return implies(f(p), (u(not(p), r)));
return implies(f(r), (u(not(p), r)));
}
/** Creates the LTLSPEC [](Q -> [](!P)) */
......@@ -145,7 +145,7 @@ public class SpecificationsFactory {
/** Creates the LTLSPEC <>R -> (P U R) */
public static IExpressionTerm universalityBeforeLTL(IExpressionTerm p, IExpressionTerm r) {
return implies(f(p), (u(p, r)));
return implies(f(r), (u(p, r)));
}
/** Creates the LTLSPEC [](Q -> [](P)) */
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment