Thanks that's helpful I'll take a look at model checking.