| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
| H A D | ibm.sml | 9 (concat hol_dir "examples/PSL/path") ::
|
| H A D | ltl2omega.sml | 8 (concat hol_dir "examples/PSL/path") ::
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
| H A D | teaScript.sml | 221 (* and needs to be visible on the search path when using or loading teaML. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
| H A D | ClockedSemanticsScript.sml | 5 (* where w is a finite or infinite word i.e. w : ('prop -> bool)path *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/ |
| H A D | example_axiomsScript.ml | 17 loadPath := "../ml" :: !loadPath; (* add acl2/ml to load path *)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
| H A D | sql.scala | 401 System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
407 def open_database(path: Path): Database =
410 val path0 = path.expand
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
| H A D | sql.scala | 401 System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
407 def open_database(path: Path): Database =
410 val path0 = path.expand
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
| H A D | binomial.tex | 17 % \path{} is the path denoting the case-study directory
21 % \def\path{\verb%Training/studies/binomial%}
74 directory \path{}:
967 at the file {\tt mk\_BINOMIAL\_integer.ml}, contained in directory \path{}.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/binomial/ |
| H A D | binomial.tex | 17 % \path{} is the path denoting the case-study directory
21 % \def\path{\verb%Training/studies/binomial%}
74 directory \path{}:
967 at the file {\tt mk\_BINOMIAL\_integer.ml}, contained in directory \path{}.
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | search.py | 379 """get the set of nodes visited on the entry path entry
406 # node i is in the set visited on the entry path, so
410 # these are visited after the head point on the entry path,
1270 (_, path) = max ([(len (data[path]), path) for path in data])
1271 models = data[path]
1274 if path2 != path])
1278 for n_vc in path
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 340 This property says that A has a winning strategy from the current state. Since we define success if the set of states satisfying the property contains the set of initial states, this suffices to check that A has a winning strategy. Cleaned up, this is the \ctl property \[ \mathbf{EG} (\textup{(A wins)} \lor (\textup{A to move} \land \mathbf{EF} (\textup{A wins})) \lor (\textup{B to move} \land \mathbf{AF} (\textup{A wins})))\] Intuitively, the property says that there exists a path from the current state such that at each step on that path either A has won the game, or it is A's turn and there exists at least one path in which A eventually wins the game, or it is not A's turn and on all paths A eventually wins the game.
402 This result corresponds to the fourth property, that stated that A has a winning strategy. This is true, and we get the success theorem, as well as a witness, which shows that there is such a path from the initial state.
490 The type constructors for \texttt{mu} \index{holCheckLib!properties!mucalculus@\(\mu\)-calculus} are shown in Table \ref{tab_mu}, together with overloaded syntax for ease of entry. For example, the property saying that there exists a path to a state where \( v_0 \land v_1 \) holds is represented by the \(\mu\)-calculus formula \( \mu Q. (v_0 \land v_1) \lor \langle.\rangle Q \) and would be written in \HOL{} as
556 The generation of witness traces for properties of the form \(\mathbf{EG} f \) (or dually, counterexamples for \(\mathbf{AF} f \) style properties) leaves much to be desired: it tries to give the shortest qualifying path which usually turns out to be just the initial state, whereas typically the user is interested in the longest one.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 340 This property says that A has a winning strategy from the current state. Since we define success if the set of states satisfying the property contains the set of initial states, this suffices to check that A has a winning strategy. Cleaned up, this is the \ctl property \[ \mathbf{EG} (\textup{(A wins)} \lor (\textup{A to move} \land \mathbf{EF} (\textup{A wins})) \lor (\textup{B to move} \land \mathbf{AF} (\textup{A wins})))\] Intuitively, the property says that there exists a path from the current state such that at each step on that path either A has won the game, or it is A's turn and there exists at least one path in which A eventually wins the game, or it is not A's turn and on all paths A eventually wins the game.
402 This result corresponds to the fourth property, that stated that A has a winning strategy. This is true, and we get the success theorem, as well as a witness, which shows that there is such a path from the initial state.
490 The type constructors for \texttt{mu} \index{holCheckLib!properties!mucalculus@\(\mu\)-calculus} are shown in Table \ref{tab_mu}, together with overloaded syntax for ease of entry. For example, the property saying that there exists a path to a state where \( v_0 \land v_1 \) holds is represented by the \(\mu\)-calculus formula \( \mu Q. (v_0 \land v_1) \lor \langle.\rangle Q \) and would be written in \HOL{} as
556 The generation of witness traces for properties of the form \(\mathbf{EG} f \) (or dually, counterexamples for \(\mathbf{AF} f \) style properties) leaves much to be desired: it tries to give the shortest qualifying path which usually turns out to be just the initial state, whereas typically the user is interested in the longest one.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
| H A D | combin.tex | 230 \path (x) edge [->,thick] node[auto,swap] {$*$} (y);
231 \path (x) edge [->,thick] node[auto] {$*$} (z);
242 \path (x) edge [->,thick] node[auto,swap] {$*$} (y);
243 \path (x) edge [->,thick] node[auto] {$*$} (z);
244 \path (y) edge [->,thick,densely dotted] node[auto,swap] {$*$} (u);
245 \path (z) edge [->,thick,densely dotted] node[auto] {$*$} (u);
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/executable-semantics/ |
| H A D | ExecuteSemanticsScript.sml | 18 loadPath := ["../../path","../../regexp","../official-semantics"] @ !loadPath;
158 (* A path is neutral iff it contains no occurrences of TOP or BOTTOM *)
1331 is "pathologically safe" [Kuperferman & Vardi 1999], meaning that the path
1382 ++ Know `!P : num -> (num -> 'a -> bool) -> ('a -> bool) path.
2129 ++ Q.PAT_ASSUM `!p : ('a -> bool) path. P p` (MP_TAC o Q.SPEC `RESTN p j`)
2288 [`n`,`LENGTH(w :('a -> bool) path)`,
|
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QbfCertificate.sml | 48 fun read_certificate_file path =
159 o QbfLibrary.read_lines_from_file) path
|
| /seL4-l4v-10.1.1/HOL4/src/pfl/ |
| H A D | index.sml | 406 in map (fn path => itlist patch binds path) plist
|
| /seL4-l4v-10.1.1/HOL4/tools-poly/ |
| H A D | configure.sml | 103 (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist);
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
| H A D | LemmasScript.sml | 21 "../official-semantics" :: "../../regexp" :: "../../path" :: !loadPath;
71 * Set default path theory to FinitePSLPathTheory
|
| /seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/ |
| H A D | proof1.ml | 107 % path state. The last step, tac4, is used to simplify the mpc state. %
|
| /seL4-l4v-10.1.1/HOL4/examples/hardware/port/tamarack2/ |
| H A D | tamarackProof1Script.sml | 113 path state. The last step, tac4, is used to simplify the mpc state. *)
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | normalForms.sml | 504 | prove_case d ((tm, path) :: rest) =
509 prove_case d ((a, (false, b) :: path) :: (b, (true, a) :: path) :: rest)
514 path
|
| H A D | folMapping.sml | 653 | hp _ _ _ = raise BUG "fol_path_to_hol" "bad higher-order path";
672 | _ => raise BUG "fol_path_to_hol" "bad eq path")
677 | _ => raise BUG "fol_path_to_hol" "bad higher-order path")
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | ReadHMF.sml | 319 map (fn p => OS.Path.mkAbsolute {path = p, relativeTo = dirname})
|
| /seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
| H A D | Help.sml | 75 (* Full path of the signature index database: *)
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/executable-semantics/ |
| H A D | ExecuteSemanticsScript.sml | 1145 is "pathologically safe" [Kuperferman & Vardi 1999], meaning that the path
1196 >> Know `!P : num -> (num -> 'a -> bool) -> ('a -> bool) path.
1943 >> Q.PAT_X_ASSUM `!p : ('a -> bool) path. P p` (MP_TAC o Q.SPEC `RESTN p j`)
2102 [`n`,`LENGTH(w :('a -> bool) path)`,
|