search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

Interpreter accepts invalid event #243

Closed lucasalbertins closed 10 years ago

lucasalbertins commented 10 years ago

The interpreter does not seem to be checking the predicates in communications. For example,

channels
    a: nat
process Test = begin
 @ a?x: (false) -> Skip
end

Process Test should not accept the communication of 'a' because the predicate is 'false', but it does.

lausdahl commented 10 years ago

Notes:

c?x:(t1) [| {c} |] c?x:(t2)
t1 : x in set {3,4}; t2 : x!= 3
c?x: (t1 and t2)

i.e. c can only take 4

for others, such as interleaving,

c?x : t1 ||| c?x : t2
c?x : t1 or t2

|||, [], |~| are the same (or) — interleaving and all non-parallels are or

only alphabetised and synchronised parallel are and, but only for those channels that are in the chansets