mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.
https://mcrl2.org/
Boost Software License 1.0
88 stars 37 forks source link

type checking ambiguities #877

Open jgroote opened 12 years ago

jgroote commented 12 years ago

Issue migrated from trac ticket # 874

component: Core: Type-checker Library | priority: major

2011-11-24 14:33:23: @wiegerw created the issue


In the following example from Jaco van de Pol there is an ambiguity in the types of the action labels:

act welke:Nat; welke:Int;

init welke(0) + welke(0);

%init sum p:Nat . (p==0) -> welke(p) % + sum p:Int . (p==0) -> welke(p);

It is undocumented how the type checker resolves such ambiguities.

jgroote commented 12 years ago

2011-11-24 17:26:16: @wiegerw commented


This is an example showing that these ambiguities lead to surprising results (supplied by Jeroen Ketema).

test3.mcrl2

act p : Nat;
act p : Int;

proc A(n : Nat, m : Int) = p(n).A(n, m) + p(m).A(n, m);

init A(0, 0);

script

act p : Nat;
act p : Int;

proc A(n : Nat, m : Int) = p(n).A(n, m) + p(m).A(n, m);

init A(0, 0);

output

[17:25:47.196 info]    LTSs are not strongly bisimilar
[17:25:47.204 info]    LTSs are not branching bisimilar
jgroote commented 12 years ago

2011-11-24 17:29:21: @wiegerw commented


(corrected copy paste error)

This is an example showing that these ambiguities lead to surprising results (supplied by Jeroen Ketema).

test3.mcrl2

act p : Nat;
act p : Int;

proc A(n : Nat, m : Int) = p(n).A(n, m) + p(m).A(n, m);

init A(0, 0);

script

mcrl22lps test3.mcrl2 test3.lps
lpspp test3.lps test4.mcrl2
mcrl22lps test4.mcrl2 test4.lps

lps2lts test3.lps test3.lts
lps2lts test4.lps test4.lts

ltscompare -ebisim test3.lts test4.lts
ltscompare -ebranching-bisim test3.lts test4.lts

output

[17:25:47.196 info]    LTSs are not strongly bisimilar
[17:25:47.204 info]    LTSs are not branching bisimilar
jgroote commented 12 years ago

2012-01-30 12:58:47: @jkeiren commented


As far as I can see, this issue can only occur in the case of the predefined numeric datatypes. In this case, observe that all ambiguities that occur in this way, may semantically be interpreted in the same way.

In user-defined cases, it is not allowed to define overloaded constructor/constants.

jgroote commented 12 years ago

2012-08-24 07:05:07:

jgroote commented 12 years ago

2012-08-24 07:05:07: commented


Milestone To be decided deleted

jgroote commented 11 years ago

2013-02-11 15:18:36: @wiegerw

jgroote commented 11 years ago

2013-02-11 15:18:36: @wiegerw commented


In a specification like the one below, the type of the expression {} is unknown. It can be either an empty set or an empty bag. This causes problems for users, since the mCRL2 language has no built-in support for disambiguation such an expression. It also causes problems for the pretty printer. After pretty printing the specification, it cannot be parsed (+ type-checked) again.

sort ID = struct i | j ;

init sum n: ID. (n in {}) -> tau <> tau ;
jgroote commented 11 years ago

2013-06-06 15:51:48: @jkeiren

jgroote commented 11 years ago

2013-08-17 11:25:07: @jgroote changed priority from minor to major

jgroote commented 11 years ago

2013-08-17 11:25:07: @jgroote

jgroote commented 11 years ago

2013-08-17 11:25:07: @jgroote commented


This problem ought to be solved with a new typechecker, following the definition in the new book. This will not be implemented in the summer 2013 release.

jgroote commented 10 years ago

2014-09-03 13:36:14: scranen@win.tue.nl commented


Pushing this issue to next year's release.

jgroote commented 10 years ago

2014-09-03 13:37:58: scranen@win.tue.nl

jgroote commented 7 years ago

2017-05-04 14:18:19: @wiegerw