{"action":"created","issue":{"url":"https://api.github.com/repos/p-org/PSharp/issues/6","labels_url":"https://api.github.com/repos/p-org/PSharp/issues/6/labels{/name}","comments_url":"https://api.github.com/repos/p-org/PSharp/issues/6/comments","events_url":"https://api.github.com/repos/p-org/PSharp/issues/6/events","html_url":"https://github.com/p-org/PSharp/issues/6","id":94222402,"number":6,"title":"Machines that don't derive from \"Machine\"","user":{"login":"paulthomson","id":5478283,"avatar_url":"https://avatars.githubusercontent.com/u/5478283?v=3","gravatar_id":"","url":"https://api.github.com/users/paulthomson","html_url":"https://github.com/paulthomson","followers_url":"https://api.github.com/users/paulthomson/followers","following_url":"https://api.github.com/users/paulthomson/following{/other_user}","gists_url":"https://api.github.com/users/paulthomson/gists{/gist_id}","starred_url":"https://api.github.com/users/paulthomson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/paulthomson/subscriptions","organizations_url":"https://api.github.com/users/paulthomson/orgs","repos_url":"https://api.github.com/users/paulthomson/repos","events_url":"https://api.github.com/users/paulthomson/events{/privacy}","received_events_url":"https://api.github.com/users/paulthomson/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/p-org/PSharp/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-07-10T06:00:35Z","updated_at":"2015-07-17T05:39:18Z","closed_at":null,"body":"One day, it might be nice to be able to create a Machine without actually having to derive from Machine. Deriving is ugly and can be problematic if you already have a class hierarchy (and you don't want to add \" : Machine\" at the top). All the (internal) machine info could be stored somewhere else. E.g. The PSharp runtime could wrap the object in a machine info object or store a mapping from the object to the machine info. The API methods can just be invoked via the PSharp runtime. As of the latest .NET, these can be imported statically so you can just type \"CreateMachine\" instead of \"PSharpRuntime.CreateMachine\" (although I quite like the latter anyway). \r\n\r\n"},"comment":{"url":"https://api.github.com/repos/p-org/PSharp/issues/comments/122181877","html_url":"https://github.com/p-org/PSharp/issues/6#issuecomment-122181877","issue_url":"https://api.github.com/repos/p-org/PSharp/issues/6","id":122181877,"user":{"login":"paulthomson","id":5478283,"avatar_url":"https://avatars.githubusercontent.com/u/5478283?v=3","gravatar_id":"","url":"https://api.github.com/users/paulthomson","html_url":"https://github.com/paulthomson","followers_url":"https://api.github.com/users/paulthomson/followers","following_url":"https://api.github.com/users/paulthomson/following{/other_user}","gists_url":"https://api.github.com/users/paulthomson/gists{/gist_id}","starred_url":"https://api.github.com/users/paulthomson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/paulthomson/subscriptions","organizations_url":"https://api.github.com/users/paulthomson/orgs","repos_url":"https://api.github.com/users/paulthomson/repos","events_url":"https://api.github.com/users/paulthomson/events{/privacy}","received_events_url":"https://api.github.com/users/paulthomson/received_events","type":"User","site_admin":false},"created_at":"2015-07-17T05:39:18Z","updated_at":"2015-07-17T05:39:18Z","body":"A static version of nondet should perhaps at least require a machineId for future-proofing. This allows each machine to have its own source of notdeterminism, which could be useful."}}