Different Answers for Cyclic Recursive Patterns using DRED and DDF

[eclipse-viatra-bot]

| --- | --- |
| Bugzilla Link | 567352 |
| Status | UNCONFIRMED |
| Importance | P3 normal |
| Reported | Sep 25, 2020 08:11 EDT |
| Modified | Oct 12, 2020 08:08 EDT |
| Version | 2.3.2 |
| Reporter | Hans van der Laan |

Description

Hey,

I have a cyclic recursive pattern and I get different results using DRED and DDF. I get a correct results with DRED and an incorrect result using DDF.
I'm not sure if it's a bug, a property of the algorithm or if I forgot to set a specific flag.

The pattern where it goes wrong deals with reachability. Specifically, with a pattern which tries to capture accessibility of security zones. We say a security zone is accessible for a given user during a given scenario if:
-case 1: the security zone is connected to the outside world and unlocked,
-case 2: the security zone connected to the outside world, protected with access control (1) and the user has the permission to access it,
-case 3: the security zone can be reached from another security zone which is accessible for this user during the given scenario and it is unlocked,
-case 4: the security zone can be reached from another security zone which is accessible for this user during the given scenario, it is protected with access control and the user has the permission to access it.

pattern SecurityZoneAccessible(user: User, scenario: java Scenario, zone: SecurityZone) {
SecurityZone.public(zone, true); // case 1
find SecurityZoneAccessStatus(scenario, zone, 0); // 0 == unlocked
User(user);
} or {
SecurityZone.public(zone, true); // case 2
find SecurityZoneAccessStatus(scenario, zone, 1); // 1 == protected with access control measures.
find USO(user, scenario, zone);
} or {
find SecurityZoneAccessStatus(scenario, zone, 0); // case 3
SecurityZone.reachable(prev,zone);
find SecurityZoneAccessible(user, scenario, prev);
} or {
find SecurityZoneAccessStatus(scenario, zone, 1); // case 4
SecurityZone.reachable(prev,zone);
find SecurityZoneAccessible(user, scenario, prev);
find USO(user, scenario, zone);
}

If we take a simple a building:

-> lobby <-> open office <-> break room

where the lobby is connected to the outside world and the open office, the open office is connected to the breakroom and the lobby and the breakroom is only connected to the open office.

If I initially say the lobby is unlocked and both the open office and the breakroom are protected with access control measures, I get the correct result when I initially compute reachability. However, if I subsequently lock the lobby DRED converges to the correct answer while DDF does not. Namely, with DRED I correctly obtain no security zone is accessible while with DDF I get that the open office and the breakroom are (still) reachable.

This reminds me of the discussion we had when I started with VIATRA about recursive patterns, the (minimal) fixed points of queries (and the happy Martians). I though DDF should be able to deal with these kinds of cases.

I create the engines as follows:

DRED:
ViatraQueryEngineOptions options = ViatraQueryEngineOptions.defineOptions()
.withDefaultBackend(DRedReteBackendFactory.INSTANCE)
.withDefaultCachingBackend(DRedReteBackendFactory.INSTANCE)
.build();

DDF:
ViatraQueryEngineOptions options = ViatraQueryEngineOptions.defineOptions()
.withDefaultBackend(TimelyReteBackendFactory.INSTANCE)
.withDefaultCachingBackend(TimelyReteBackendFactory.INSTANCE)
.build();

[eclipse-viatra-bot]

By Hans van der Laan on Oct 12, 2020 08:00

Can anyone confirm if this is a bug or intended behaviour?

[eclipse-viatra-bot]

By Zoltan Ujhelyi on Oct 12, 2020 08:08

(In reply to Hans van der Laan from comment #1)

Can anyone confirm if this is a bug or intended behaviour?

Sorry for the late response. Gábor Bergmann was on vacation, and with regards these deep algorithmic question he would be the best person to answer. There are some corner cases that some algorithm supports but the other not. My expectation would be that the result should not depend on the algorithms, but I am not entirely sure about that.