{"action":"created","issue":{"url":"https://api.github.com/repos/fscheck/FsCheck/issues/107","labels_url":"https://api.github.com/repos/fscheck/FsCheck/issues/107/labels{/name}","comments_url":"https://api.github.com/repos/fscheck/FsCheck/issues/107/comments","events_url":"https://api.github.com/repos/fscheck/FsCheck/issues/107/events","html_url":"https://github.com/fscheck/FsCheck/issues/107","id":88763347,"number":107,"title":"How to do model based testing?","user":{"login":"forki","id":57396,"avatar_url":"https://avatars.githubusercontent.com/u/57396?v=3","gravatar_id":"","url":"https://api.github.com/users/forki","html_url":"https://github.com/forki","followers_url":"https://api.github.com/users/forki/followers","following_url":"https://api.github.com/users/forki/following{/other_user}","gists_url":"https://api.github.com/users/forki/gists{/gist_id}","starred_url":"https://api.github.com/users/forki/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/forki/subscriptions","organizations_url":"https://api.github.com/users/forki/orgs","repos_url":"https://api.github.com/users/forki/repos","events_url":"https://api.github.com/users/forki/events{/privacy}","received_events_url":"https://api.github.com/users/forki/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-06-16T15:41:04Z","updated_at":"2015-06-17T07:59:11Z","closed_at":null,"body":"i came across John Hughes' excellent video from https://vimeo.com/68383317 and tried to reimplement his first sample. It's similar to https://fscheck.github.io/FsCheck/StatefulTesting.html but a little bit more complicated. This is the class I want to test:\r\n\r\n    type Queue<'a>(bufferSize:int) =\r\n        let mutable input = 0\r\n        let mutable output = 0\r\n        let buffer : 'a[] = Array.zeroCreate bufferSize\r\n\r\n        member __.Put x = \r\n            buffer.[input] <- x\r\n            input <- (input + 1) % bufferSize\r\n\r\n        member __.Get() = \r\n            let x = buffer.[output]\r\n            output <- (output + 1) % bufferSize\r\n            x\r\n\r\n        member __.Size() = (input - output) % bufferSize\r\n\r\nNow I tried to define the model:\r\n\r\n    let spec =\r\n      let put testElement =\r\n          { new Command<Queue<int>,_>() with\r\n              member x.RunActual c =  c.Put testElement; c\r\n              member x.RunModel m = m @ [testElement]\r\n              member x.Post (c,m) = List.head m = c.Get() |> Prop.ofTestable // calling Get??\r\n              override x.ToString() = \"put\"}\r\n\r\n      let get = \r\n          { new Command<Queue<int>,_>() with\r\n              member x.RunActual c = c.Get(); c\r\n              member x.RunModel m = List.tail m\r\n              member x.Post (c,m) =  List.head m = c.Get() |> Prop.ofTestable // calling Get twice??\r\n              override x.ToString() = \"get\"}\r\n\r\n      { new ICommandGenerator<Queue<int>,_> with\r\n          member __.InitialActual = Queue(1) /// n??\r\n          member __.InitialModel = []\r\n          member __.Next model = Gen.elements [put (*random element *) ;get] }\r\n\r\n\r\n    Check.Quick (Command.toProperty spec)\r\n\r\nBut this fails for a couple of reasons. \r\n\r\n1) If I understand the video at 10min correctly the RunActual function should capture the method result and the new `Actual`. This would allow me to specify the correct post condition.\r\n\r\n2) how can I generate operations that put random elements?\r\n\r\n3) how can I generate queues with random buffer sizes?"},"comment":{"url":"https://api.github.com/repos/fscheck/FsCheck/issues/comments/112705853","html_url":"https://github.com/fscheck/FsCheck/issues/107#issuecomment-112705853","issue_url":"https://api.github.com/repos/fscheck/FsCheck/issues/107","id":112705853,"user":{"login":"kurtschelfthout","id":164917,"avatar_url":"https://avatars.githubusercontent.com/u/164917?v=3","gravatar_id":"","url":"https://api.github.com/users/kurtschelfthout","html_url":"https://github.com/kurtschelfthout","followers_url":"https://api.github.com/users/kurtschelfthout/followers","following_url":"https://api.github.com/users/kurtschelfthout/following{/other_user}","gists_url":"https://api.github.com/users/kurtschelfthout/gists{/gist_id}","starred_url":"https://api.github.com/users/kurtschelfthout/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kurtschelfthout/subscriptions","organizations_url":"https://api.github.com/users/kurtschelfthout/orgs","repos_url":"https://api.github.com/users/kurtschelfthout/repos","events_url":"https://api.github.com/users/kurtschelfthout/events{/privacy}","received_events_url":"https://api.github.com/users/kurtschelfthout/received_events","type":"User","site_admin":false},"created_at":"2015-06-17T07:59:10Z","updated_at":"2015-06-17T07:59:10Z","body":"Yeah, I'll change 1 and 3."}}