Re: [Rodin-b-sharp-user] progress & liveness properties?

[Thái S. H. <ts...@us...>]

 Dear Marko,
 There is no easy way to simulate "M leads from P1 to P2" excepts to encode
the condition as theorems in the machine M to prove that every events in M
leads from P1 to P2.
 "M is convergent in P" is easier to simulate, by making a refinement of M,
add P as additional guard of all events, then prove that all events are
convergent using some variant. Often, this convergence proof is done in
several refinements (lexicographic variant). It is usually difficult to
find a single variant for many events.
 "M is deadlock-free in P" should also be encoded as a theorem (similar to
standard DLF in Event-B)
 That should be enough for proving progress properties.
 Best regards,
Son


2014-06-11 0:03 GMT+09:00 Marko Schütz Schmuck <Mar...@we...>:

> Dear All,
>
> I found the paper "Reasoning about Liveness Properties in Event-B" by
> Hoang and Abrial. I was wondering whether there is a technical report
> that has more detail particularly on the simulation of the concepts
> within Rodin. For example, how to simulate "M leads from P1 to P2".
>
> Thanks and best regards,
>
> Marko
>
> ------------------------------------------------------------------------------
> HPCC Systems Open Source Big Data Platform from LexisNexis Risk Solutions
> Find What Matters Most in Your Big Data with HPCC Systems
> Open Source. Fast. Scalable. Simple. Ideal for Dirty Data.
> Leverages Graph Analysis for Fast Processing & Easy Data Exploration
> http://p.sf.net/sfu/hpccsystems
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>
>