mCRL2
mCRL2 copied to clipboard
mCRL2org
type checking ambiguities
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.
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
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
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.
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 ;
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.