## rodin-b-sharp-user

 [Rodin-b-sharp-user] Problem to Assigning Non-deterministic Values From: Thiago Carvalho de Sousa - 2012-11-26 23:51:25 ```Hi my friends, It seems I have a very stupid issue, but I can not figure out what is wrong. I get the error "Syntax error: Expected: :∈ but was: ( " when I try to define an non-deterministic action like that: event nondeterministic any a where a ∈ aa then lifespan(a) :∈ {x,y} end variables aa ∈ ℙ(AAA_SET) lifespan ∈ aa → Status sets AAA_SET Status constants x y axioms partition(Status, {x},{y}) When I try "lifespan(a) := x" or "lifespan(a) := y" works fine. Any workaround for that!!?? Thanks in advance, Thiago ```
 Re: [Rodin-b-sharp-user] Problem to Assigning Non-deterministic Values From: Hoang, Thai Son - 2012-11-27 05:49:14 ``` Dear Thiago, The only substitution supporting f(x) on the left-hand side is deterministic one, i.e. with :=. In fact, f(x) := E is only a short-cut for f := f <+ {x |-> E}. In your case, it is better to have another parameter to indicate the possible value for lifespan(a), e.g. b. event nondeterministic any a, b where a : aa b : {x, y} then lifespan(a) := b end Cheers, Son On 27 Nov 2012, at 00:51, Thiago Carvalho de Sousa wrote: > Hi my friends, > > It seems I have a very stupid issue, but I can not figure out what is > wrong. I get the error > "Syntax error: Expected: :∈ but was: ( " when I try to define an > non-deterministic action like that: > > event nondeterministic > any a > where a ∈ aa > then lifespan(a) :∈ {x,y} > end > > variables > aa ∈ ℙ(AAA_SET) > lifespan ∈ aa → Status > > sets > AAA_SET > Status > > constants > x > y > > axioms > partition(Status, {x},{y}) > > When I try "lifespan(a) := x" or "lifespan(a) := y" works fine. Any > workaround for that!!?? > > Thanks in advance, > > Thiago > > ------------------------------------------------------------------------------ > Monitor your physical, virtual and cloud infrastructure from a single > web console. Get in-depth insight into apps, servers, databases, vmware, > SAP, cloud infrastructure, etc. Download 30-day Free Trial. > Pricing starts from \$795 for 25 servers or applications! > http://p.sf.net/sfu/zoho_dev2dev_nov > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Problem to Assigning Non-deterministic Values From: Laurent Voisin - 2012-11-28 12:34:23 ```Dear Thiago, coming back to the excellent answers from Daniel and Son (who independently reached the same conclusion), I would just like to emphasize why the syntactic sugar you were trying to use is not implemented. In the general case, a non-deterministic assignment written f(x) :∈ A would be syntactic sugar for the assignment f :∈ {y · y ∈ A ∣ f <+ {x ↦ y}} This latter expression is complicated enough that we deemed it would be a bad idea to propose such syntactic sugar. Best Regards, Laurent. Le 27 nov. 2012 à 06:49, Hoang, Thai Son a écrit : > Dear Thiago, > The only substitution supporting f(x) on the left-hand side is deterministic one, i.e. with :=. In fact, f(x) := E is only a short-cut for f := f <+ {x |-> E}. > In your case, it is better to have another parameter to indicate the possible value for lifespan(a), e.g. b. > event nondeterministic > any a, b > where > a : aa > b : {x, y} > then > lifespan(a) := b > end > Cheers, > Son > On 27 Nov 2012, at 00:51, Thiago Carvalho de Sousa wrote: > >> Hi my friends, >> >> It seems I have a very stupid issue, but I can not figure out what is >> wrong. I get the error >> "Syntax error: Expected: :∈ but was: ( " when I try to define an >> non-deterministic action like that: >> >> event nondeterministic >> any a >> where a ∈ aa >> then lifespan(a) :∈ {x,y} >> end >> >> variables >> aa ∈ ℙ(AAA_SET) >> lifespan ∈ aa → Status >> >> sets >> AAA_SET >> Status >> >> constants >> x >> y >> >> axioms >> partition(Status, {x},{y}) >> >> When I try "lifespan(a) := x" or "lifespan(a) := y" works fine. Any >> workaround for that!!?? >> >> Thanks in advance, >> >> Thiago >> >> ------------------------------------------------------------------------------ >> Monitor your physical, virtual and cloud infrastructure from a single >> web console. Get in-depth insight into apps, servers, databases, vmware, >> SAP, cloud infrastructure, etc. Download 30-day Free Trial. >> Pricing starts from \$795 for 25 servers or applications! >> http://p.sf.net/sfu/zoho_dev2dev_nov >> _______________________________________________ >> Rodin-b-sharp-user mailing list >> Rodin-b-sharp-user@... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > ------------------------------------------------------------------------------ > Monitor your physical, virtual and cloud infrastructure from a single > web console. Get in-depth insight into apps, servers, databases, vmware, > SAP, cloud infrastructure, etc. Download 30-day Free Trial. > Pricing starts from \$795 for 25 servers or applications! > http://p.sf.net/sfu/zoho_dev2dev_nov > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Problem to Assigning Non-deterministic Values From: Daniel Plagge - 2012-11-27 06:08:55 ```Hello Thiago, the problem is that the syntax allows you to use the form "f(x) := y" or "x :: S", but you cannot combine it (syntactically) to "f(x) :: S". Please note that "f(x) := y" is just syntactic sugar for "f := f <+ {x|->y}". I see two options here: * use "lifespan :: {lifespan <+ {a|->x}, lifespan <+ {a|->y}" or * introduce another parameter event nondeterministic any a z where a ∈ aa & z : {x,y} then lifespan(a) := z end I think the second one is more readable. Best regards Daniel Am 27.11.2012 00:51, schrieb Thiago Carvalho de Sousa: > Hi my friends, > > It seems I have a very stupid issue, but I can not figure out what is > wrong. I get the error > "Syntax error: Expected: :∈ but was: ( " when I try to define an > non-deterministic action like that: > > event nondeterministic > any a > where a ∈ aa > then lifespan(a) :∈ {x,y} > end > > variables > aa ∈ ℙ(AAA_SET) > lifespan ∈ aa → Status > > sets > AAA_SET > Status > > constants > x > y > > axioms > partition(Status, {x},{y}) > > When I try "lifespan(a) := x" or "lifespan(a) := y" works fine. Any > workaround for that!!?? > > Thanks in advance, > > Thiago > > ------------------------------------------------------------------------------ > Monitor your physical, virtual and cloud infrastructure from a single > web console. Get in-depth insight into apps, servers, databases, vmware, > SAP, cloud infrastructure, etc. Download 30-day Free Trial. > Pricing starts from \$795 for 25 servers or applications! > http://p.sf.net/sfu/zoho_dev2dev_nov > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```