Model checking of Reo models with mcrl2 - DoorController mcrl2 specifovation

[Alireza Farhadi]

Dear Christian,

When I read Natallia recommended paper ( http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf) I faced an example of mcrl2 internal specification of a component named DoorController that Reo model and equivalent mcrl2 specification are attached.

In this specification firstly lock action happened at time t then unlock occurred at time t+ theta but in the Reo model after filling a fifo1, a token firstly received to unlock node then after theta elapsed the token received to lock node.

Can you explain about this contradiction?

Regards,

Alireza Farhadi

[christian]

Hi Alireza,
was issue finally resolved?

Cheers,
Christian

On Oct 22, 11:41 am, Alireza Farhadi <alireza.farh...@gmail.com>
wrote:
> Dear Christian,
>
> When I read Natallia recommended paper (http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf) I faced an example of

>  DoorController.PNG
> 20KViewDownload

[Natallia Kokash]

Dear Christian,

I probably forgot to include you in the CC of my message, but I replied to Alireza.
He is right, there was a typo in the system: in the mcrl specification of DoorController there should be first unlock and then lock.

Regards,
Natallia

Cheers,
Christian

--
You received this message because you are subscribed to the Google Groups "reo-dev" group.
To post to this group, send email to reo...@googlegroups.com.
To unsubscribe from this group, send email to reo-dev+u...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/reo-dev?hl=en.

[Alireza Farhadi]

Dear Natallia and Cristian,

Thanks for you attention to my problem.

Regards,

Alireza Farhadi

[Alireza Farhadi]

Dear Natallia, Christian:

In your paper ( http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf)
you mentioned an optimized version of access control system sample that can
handle asynchronous receiving of authentication and authorization
component response.

When I see Reo network of optimized ACS (Acess Control System) sample
I found a difference between type of nodes that are received
authenticate and authorize nOkOut component response in
CenteralStation component, respectively there exist a replicate node
for nOkOut of authenticate component and a rout node for nOkOut of
authorize component.

I want to point an issue when firstly PanelControl component send
pId==2 that caused entrance is not allowed if firstly authorize nOkOut
response received to corresponding input rout node in CenteralStation
component then authenticate nOkOut fired consequently one token
(authenticate nOkOut) remains in FIFO1 channel connected to
corresponding replicate input node in CenteralStation. This remained
token disturbs operation of network for next pId==1, this pId must be
allowed for entrance but when authenticate and authorize okOut
responses are provided synchronously, this remained token not allowed
corresponding rout input node for okOut of authorize component can any
action. by this way all CentralStation network is hanged.

I guess this situation is deadlock, I checked deadlock freedom mu
calculus property "[true*]<true>true" over optimized ACS sample mcrl2
encoding caused false result but in previous version (exact ACS)
sample this property (deadlock freedom is satisfied). this show to me
translation of reo to mcrl2 is correct (although this is proved).

I want a mu calculus more specific property that specify this
difference between 2 versions of ACS sample because deadlock freedom
is very general, Is there any suggestion for that? I'm newbie to mu
calculus.

image of 2 version of this ACS sample is attached.

Regards
Alireza Farhadi

[Christian Krause]

Dear Alireza,

thank you for your comments on the example.

Regarding help and examples for mu-calculus formulae, you can check out these man-pages:

http://mcrl2.org/mcrl2/wiki/index.php?title=Language_reference/Modal_formulas

http://www.inrialpes.fr/vasy/cadp/man/evaluator.html

For specific question you can also try asking at the mCRL2-users mailing list.

Cheers,
Christian

[Alireza Farhadi]

Dear Christian,
Thanks for your attention.
When i read
http://mcrl2.org/mcrl2/wiki/index.php?title=Language_reference/Modal_formulas

I think there is a typo in "Relations between symbols" section

[φr|ψr]φs = [φr]φs && [ψr]φs must be [φr+ψr]φs = [φr]φs && [ψr]φs

and

<φr|ψr>φs = <φr>φs || <φr>φs must be <φr+ψr>φs = <φr>φs || <φr>φs

Is that correct? Multi-action operator "|" is not defined for regular
formula, I guess choice operation must be correct.

Regards
Alireza Farhadi

[Christian Krause]

Hi Alireza,

I cannot tell without looking into it in more detail. Please use the
mCRL2 mailing list for this sort of question. I am sure they can help you.

Cheers,
Christian

On 18.11.2011 06:43, Alireza Farhadi wrote:
> Dear Christian,
> Thanks for your attention.
> When i read
> http://mcrl2.org/mcrl2/wiki/index.php?title=Language_reference/Modal_formulas
>
> I think there is a typo in "Relations between symbols" section
>

> [οΏ½r|οΏ½r]οΏ½s = [οΏ½r]οΏ½s&& [οΏ½r]οΏ½s must be [οΏ½r+οΏ½r]οΏ½s = [οΏ½r]οΏ½s&& [οΏ½r]οΏ½s
>
> and
>
> <οΏ½r|οΏ½r>οΏ½s =<οΏ½r>οΏ½s ||<οΏ½r>οΏ½s must be<οΏ½r+οΏ½r>οΏ½s =<οΏ½r>οΏ½s ||<οΏ½r>οΏ½s

[Alireza Farhadi]

OK Dear Christian

I found that in second your mu-calculus references "I" means for
choice operator in regular formula and in some others "+" means for
that.

Thanks and Regards,
Alireza Farhadi

On 11/18/11, Christian Krause <hensh...@gmail.com> wrote:
> Hi Alireza,
>
> I cannot tell without looking into it in more detail. Please use the
> mCRL2 mailing list for this sort of question. I am sure they can help you.
>
> Cheers,
> Christian
>
> On 18.11.2011 06:43, Alireza Farhadi wrote:
>> Dear Christian,
>> Thanks for your attention.
>> When i read
>> http://mcrl2.org/mcrl2/wiki/index.php?title=Language_reference/Modal_formulas
>>
>> I think there is a typo in "Relations between symbols" section
>>

>> [φr|ψr]φs = [φr]φs&& [ψr]φs must be [φr+ψr]φs = [φr]φs&& [ψr]φs

>>
>> and
>>
>> <φr|ψr>φs =<φr>φs ||<φr>φs must be<φr+ψr>φs =<φr>φs ||<φr>φs
>>