{"action":"created","issue":{"url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/1237","repository_url":"https://api.github.com/repos/mCRL2org/mCRL2","labels_url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/1237/labels{/name}","comments_url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/1237/comments","events_url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/1237/events","html_url":"https://github.com/mCRL2org/mCRL2/issues/1237","id":326659705,"node_id":"MDU6SXNzdWUzMjY2NTk3MDU=","number":1237,"title":"Pretty printer/lineariser omits explicit typecasts","user":{"login":"jgroote","id":9032656,"node_id":"MDQ6VXNlcjkwMzI2NTY=","avatar_url":"https://avatars3.githubusercontent.com/u/9032656?v=4","gravatar_id":"","url":"https://api.github.com/users/jgroote","html_url":"https://github.com/jgroote","followers_url":"https://api.github.com/users/jgroote/followers","following_url":"https://api.github.com/users/jgroote/following{/other_user}","gists_url":"https://api.github.com/users/jgroote/gists{/gist_id}","starred_url":"https://api.github.com/users/jgroote/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jgroote/subscriptions","organizations_url":"https://api.github.com/users/jgroote/orgs","repos_url":"https://api.github.com/users/jgroote/repos","events_url":"https://api.github.com/users/jgroote/events{/privacy}","received_events_url":"https://api.github.com/users/jgroote/received_events","type":"User","site_admin":false},"labels":[{"id":893782244,"node_id":"MDU6TGFiZWw4OTM3ODIyNDQ=","url":"https://api.github.com/repos/mCRL2org/mCRL2/labels/bug","name":"bug","color":"d73a4a","default":true}],"state":"closed","locked":false,"assignee":{"login":"wiegerw","id":1238689,"node_id":"MDQ6VXNlcjEyMzg2ODk=","avatar_url":"https://avatars0.githubusercontent.com/u/1238689?v=4","gravatar_id":"","url":"https://api.github.com/users/wiegerw","html_url":"https://github.com/wiegerw","followers_url":"https://api.github.com/users/wiegerw/followers","following_url":"https://api.github.com/users/wiegerw/following{/other_user}","gists_url":"https://api.github.com/users/wiegerw/gists{/gist_id}","starred_url":"https://api.github.com/users/wiegerw/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wiegerw/subscriptions","organizations_url":"https://api.github.com/users/wiegerw/orgs","repos_url":"https://api.github.com/users/wiegerw/repos","events_url":"https://api.github.com/users/wiegerw/events{/privacy}","received_events_url":"https://api.github.com/users/wiegerw/received_events","type":"User","site_admin":false},"assignees":[{"login":"wiegerw","id":1238689,"node_id":"MDQ6VXNlcjEyMzg2ODk=","avatar_url":"https://avatars0.githubusercontent.com/u/1238689?v=4","gravatar_id":"","url":"https://api.github.com/users/wiegerw","html_url":"https://github.com/wiegerw","followers_url":"https://api.github.com/users/wiegerw/followers","following_url":"https://api.github.com/users/wiegerw/following{/other_user}","gists_url":"https://api.github.com/users/wiegerw/gists{/gist_id}","starred_url":"https://api.github.com/users/wiegerw/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wiegerw/subscriptions","organizations_url":"https://api.github.com/users/wiegerw/orgs","repos_url":"https://api.github.com/users/wiegerw/repos","events_url":"https://api.github.com/users/wiegerw/events{/privacy}","received_events_url":"https://api.github.com/users/wiegerw/received_events","type":"User","site_admin":false}],"milestone":null,"comments":7,"created_at":"2013-11-22T10:46:25Z","updated_at":"2018-07-11T08:47:10Z","closed_at":"2018-07-11T08:09:55Z","author_association":"MEMBER","body":"*Issue migrated from trac ticket # 1236*\n\n**component:** Core: Type-checker Library | **priority:** major\n\n#### 2013-11-22 10:46:25: @twillems created the issue\n\n\n___\nThe lineariser or the pretty printer omit explicit typecasts in converting mCRL2 files. \n\nUnder certain circumstances, this can introduce type checking errors in the mCRL2 files obtained by linearising and subsequent pretty printing. A small example illustrating the issues is the following:\n\n```\nsort A = struct element(id:Nat);\n\nmap f: A -> Int;\nvar a:A; id:Nat;\neqn \nf(a) = Nat2Int(id(a));\n\ninit delta;\n```\n\nAfter linearising and pretty-printing the above specification, the resulting code is no longer linearisable. Reusing function names (id) as variable names (id) appears to be a prerequisite in reproducing the issue.\n"},"comment":{"url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/comments/404093235","html_url":"https://github.com/mCRL2org/mCRL2/issues/1237#issuecomment-404093235","issue_url":"https://api.github.com/repos/mCRL2org/mCRL2/issues/1237","id":404093235,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNDA5MzIzNQ==","user":{"login":"tneele","id":3605951,"node_id":"MDQ6VXNlcjM2MDU5NTE=","avatar_url":"https://avatars1.githubusercontent.com/u/3605951?v=4","gravatar_id":"","url":"https://api.github.com/users/tneele","html_url":"https://github.com/tneele","followers_url":"https://api.github.com/users/tneele/followers","following_url":"https://api.github.com/users/tneele/following{/other_user}","gists_url":"https://api.github.com/users/tneele/gists{/gist_id}","starred_url":"https://api.github.com/users/tneele/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tneele/subscriptions","organizations_url":"https://api.github.com/users/tneele/orgs","repos_url":"https://api.github.com/users/tneele/repos","events_url":"https://api.github.com/users/tneele/events{/privacy}","received_events_url":"https://api.github.com/users/tneele/received_events","type":"User","site_admin":false},"created_at":"2018-07-11T08:47:10Z","updated_at":"2018-07-11T08:47:10Z","author_association":"COLLABORATOR","body":"The variable `id` is not relevant to the problem at all, so the bug is still there. Take for example the following specification:\r\n```\r\nsort A = struct element(id:Nat);\r\n\r\nmap f: A -> Int;\r\nvar a:A;\r\neqn \r\nf(a) = Nat2Int(id(a));\r\n\r\ninit delta;\r\n```\r\nRunning the following command sequence yields:\r\n```\r\n$ mcrl22lps test.mcrl2 | lpspp | mcrl22lps > test2.lps\r\n[error]   Types of the left- (Int) and right- (Nat) hand-sides of the equation f(a)  =  id(a) do not match.\r\n[error]   Failed to type check data specification.\r\n```\r\nIn my opinion, this is a valid use case, so the issue should be fixed."}}
{"actor":{"display_login":"tneele"}}