|
(* Title: HOL/Nitpick_Examples/Hotel_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2010-2011
Nitpick example based on Tobias Nipkow's hotel key card formalization.
*)
section \<open>Nitpick Example Based on Tobias Nipkow's Hotel Key Card
Formalization\<close>
theory Hotel_Nits
imports Main
begin
nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
max_threads = 1, timeout = 240]
typedecl guest
typedecl key
typedecl room
type_synonym keycard = "key \ key"
record state =
owns :: "room \ guest option"
currk :: "room \ key"
issued :: "key set"
cards :: "guest \ keycard set"
roomk :: "room \ key"
isin :: "room \ guest set"
safe :: "room \ bool"
inductive_set reach :: "state set" where
init:
"inj initk \
\<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
check_in:
"\s \ reach; k \ issued s\ \
s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
owns := (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
enter_room:
"\s \ reach; (k,k') \ cards s g; roomk s r \ {k,k'}\ \
s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
roomk := (roomk s)(r := k'),
safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<^cancel>\<open>\<and> k' = currk s r\<close>
\<or> safe s r)\<rparr> \<in> reach" |
exit_room:
"\s \ reach; g \ isin s r\ \ s\isin := (isin s)(r := isin s r - {g})\ \ reach"
theorem safe: "s \ reach \ safe s r \ g \ isin s r \ owns s r = Some g"
nitpick [card room = 1, card guest = 2, card "guest option" = 3,
card key = 4, card state = 6, show_consts, format = 2,
expect = genuine]
(* nitpick [card room = 1, card guest = 2, expect = genuine] *) (* slow *)
oops
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
