Action synchronization broken in PTAs?

[c-kloukinas]

Hi, I'm getting a behaviour that seems to indicate that action synchronization is broken in PTAs (unlike DTMC). Here's a simple model, where I'd expect the results to be the same for PTA and DTMC but PTA seems to allow a blocked action in one module to occur in another - see the probability 1.0 for eventually seenA, which I'd expect to be 0.0, as in the DTMC model.

Best, Christos

// dtmc // Pmax =? [ F seenA ] = 0.0 Pmax =? [ F seenB ] = 0.0 pta // Pmax =? [ F seenA ] = 1.0 Pmax =? [ F seenB ] = 0.0

module AA seenA: bool init false;

[fire] true -> (seenA'=true); endmodule

module BB seenB: bool init false;

[fire] false -> (seenB'=true); endmodule

[kleinj]

Hi,

I can confirm that there's something wrong.

With -ptamethod games (default PTA method):

$ prism pta.prism -pf 'Pmax=?[ F seenA ]; Pmax=?[ F seenB ]' -exportresults stdout --ptamethod games

Exporting results below:

Pmax=? [ F seenA ]:
Result
1.0

Pmax=? [ F seenB ]:
Result
0.0

With -ptamethod digital (alternative PTA method):

$ prism pta.prism -pf 'Pmax=?[ F seenA ]; Pmax=?[ F seenB ]' -exportresults stdout --ptamethod digital

Exporting results below:

Pmax=? [ F seenA ]:
Result
0.0

Pmax=? [ F seenB ]:
Result
0.0

[kleinj]

Ok, after some debugging, it looks like this is what happens: The alphabet information (i.e., which synchronizing actions occur in each module) for the generated PTA for a module is derived from the actions that actually exist, i.e., those with a false guard are already filtered out.

For a fix, the alphabet information should probably be derived from the original module information instead.

[c-kloukinas]

Hi, I thought that something like this might be the case - e.g., that's how the LTSA tool works for FSP that I'm more familiar with. But in FSP they also provide you with alphabet extension, so that you can add an action to a module to keep other modules from executing it - in Prism I didn't see something like that supported. Plus, it seems that this behaviour is only for PTAs with a specific engine (maybe more?), so it looks like an inconsistency.

BTW - the alphabet extension operator would be a very nice addition, as it'd allow a specifier to clearly document the actions of the module's API in the model and cause some nice deadlocks if there's a bug in the model. Being able to declare the actions as a set (so as not to repeat them by copy-pasting) would help in catching typos.

Oh, and thanks for all the work on Prism - great tool! :-)

Cheers, Christos

On 05/09/16 15:41, Joachim Klein wrote:

Ok, after some debugging, it looks like this is what happens: The alphabet information (i.e., which synchronizing actions occur in each module) for the generated PTA for a module is derived from the actions that actually exist, i.e., those with a false guard are already filtered out.

For a fix, the alphabet information should probably be derived from the original module information instead.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/prismmodelchecker/prism/issues/10#issuecomment-244762343, or mute the thread https://github.com/notifications/unsubscribe-auth/AGu4xF-kl5z2Jr_6XmaW1Yv-s0a2d_swks5qnCokgaJpZM4J1GFp.

[davexparker]

Thanks both. Yes, the definition of a module's alphabet should be syntactic. This means that the behaviour observed here with the PTA model checker (and the games engine) is a bug.

Although we don't have a clean way of specify/extending the alphabet, a simple trick I have used before is to add commands such as:

[a] false -> true;

This adds a to the alphabet of the module, without actually adding a-labelled transitions to the semantic model. Obviously this only works for PTAs of this bug is fixed...