Searched refs:model (Results 1 - 25 of 314) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DholCheck.sig4 val holCheck : modelTools.model -> modelTools.model
H A DholCheckLib.sig6 type model = modelTools.model type
8 val holCheck : model -> model
12 val empty_model : model
14 val set_init : Term.term -> model -> model
15 val set_trans : (string * Term.term) list -> model -> model
16 val set_flag_ric : bool -> model
[all...]
H A DmodelTools.sig6 type model type
9 val empty_model : model
11 val get_init : model -> Term.term
12 val get_trans : model ->(string * Term.term) list
13 val get_flag_ric : model -> bool
14 val get_name : model -> string option
15 val get_vord : model -> string list option
16 val get_state : model -> Term.term option
17 val get_props : model -> (string * Term.term) list
18 val get_results : model
[all...]
H A DmodelTools.sml2 (* this contains all info about the model, including the properties to be checked, and th eventual results *)
21 type model = {init: term option, type
37 fun get_name (m:model) = #name(m)
38 fun get_init (m:model) = valOf (#init(m))
39 fun get_trans (m:model) = valOf (#trans(m))
40 fun get_flag_ric (m:model) = valOf (#ric(m))
41 fun get_vord (m:model) = #vord(m)
42 fun get_state (m:model) = #state(m)
43 fun get_props (m:model) = valOf (#props(m))
44 fun get_results (m:model)
[all...]
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/machine/
H A Dtimer.h16 #include <arch/model/statedata.h>
/seL4-l4v-10.1.1/seL4/src/config/
H A Ddefault_domain.c12 #include <model/statedata.h>
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibModel.sig13 (* The parts of the model that are fixed and cannot be perturbed *)
14 (* Note: a model of size N has integer elements 0...N-1 *)
34 type model type
37 val new : parameters -> model
38 val size : model -> int
41 val evaluate_term : model -> term -> int
42 val evaluate_formula : model -> formula -> bool
44 (* Check whether a random grounding of a formula is satisfied by the model *)
45 val check : model -> formula -> bool
46 val checkn : model
[all...]
/seL4-l4v-10.1.1/seL4/include/model/
H A Dsmp.h18 #include <arch/model/statedata.h>
19 #include <model/statedata.h>
/seL4-l4v-10.1.1/seL4/src/model/
H A Dpreemption.c12 #include <model/preemption.h>
13 #include <model/statedata.h>
H A Dsmp.c14 #include <model/smp.h>
/seL4-l4v-10.1.1/l4v/spec/cspec/c/
H A Dconfig_sched.c12 #include <model/statedata.h>
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/model/
H A Dsmp.h18 #include <arch/model/statedata.h>
19 #include <model/statedata.h>
20 #include <model/smp.h>
21 #include <mode/model/smp.h>
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DModel.sig16 (* A model of size N has integer elements 0...N-1. *)
26 (* The parts of the model that are fixed. *)
55 (* Renaming fixed model parts. *)
67 (* Standard fixed model parts. *)
202 type model type
206 val new : parameters -> model
208 val size : model -> int
211 (* Interpreting terms and formulas in the model. *)
214 val interpretFunction : model -> Term.functionName * element list -> element
216 val interpretRelation : model
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DModel.sig16 (* A model of size N has integer elements 0...N-1. *)
26 (* The parts of the model that are fixed. *)
55 (* Renaming fixed model parts. *)
67 (* Standard fixed model parts. *)
202 type model type
206 val new : parameters -> model
208 val size : model -> int
211 (* Interpreting terms and formulas in the model. *)
214 val interpretFunction : model -> Term.functionName * element list -> element
216 val interpretRelation : model
[all...]
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/
H A Dcpu_identification.c14 /** @file Support routines for identifying the processor family, model, etc
15 * on INTEL x86 processors, as well as attempting to determine the model string.
57 uint8_t family, model; member in struct:family_model
65 * require you to take into account an additional extended family and model
84 * Additionally, even though the Intel manuals say to adjust the model
96 ci->display.model = (ci->display.extended_model << 4u) + original.model;
98 ci->display.model = original.model;
107 * the family and model ID
[all...]
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/model/
H A Dstatedata.h16 #include <model/statedata.h>
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/
H A Dvscode_resources.scala50 (_, model) <- models.iterator
51 blob <- model.get_blob
52 } yield (model.node_name -> blob)).toMap)
66 sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
68 def node_name: Document.Node.Name = model.node_name
134 case Some(model) => Some(model.content.text)
142 case Some(model) => f(Scan.char_reader(model.content.text))
156 case Some(model)
[all...]
H A Dpreview_panel.scala29 case Some(model) =>
30 val snapshot = model.snapshot()
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/
H A Dvscode_resources.scala50 (_, model) <- models.iterator
51 blob <- model.get_blob
52 } yield (model.node_name -> blob)).toMap)
66 sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
68 def node_name: Document.Node.Name = model.node_name
134 case Some(model) => Some(model.content.text)
142 case Some(model) => f(Scan.char_reader(model.content.text))
156 case Some(model)
[all...]
H A Dpreview_panel.scala29 case Some(model) =>
30 val snapshot = model.snapshot()
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DtemporalScript.sml33 SPEC_1 model pre code post err <=>
34 TEMPORAL model code
40 val INIT = `?to_set next instr less allow. model = (to_set,next,instr,less,allow)`
44 `SPEC model pre code post <=>
45 TEMPORAL model code (T_IMPLIES (NOW pre) (EVENTUALLY (NOW post)))`,
54 `TEMPORAL model code (ALWAYS p) <=> TEMPORAL model code p`,
74 `TEMPORAL model code (T_IMPLIES p1 (NEXT p2)) ==>
75 TEMPORAL model code (T_IMPLIES p1 (EVENTUALLY p2))`,
82 ``SPEC_1 model pr
[all...]
/seL4-l4v-10.1.1/seL4/src/plat/pc99/machine/
H A Dhardware.c14 #include <arch/model/statedata.h>
99 if (model_info->model == valid_models[i]) {
111 if (model_info->model == NEHALEM_1_MODEL_ID ||
112 model_info->model == NEHALEM_2_MODEL_ID ||
113 model_info->model == NEHALEM_3_MODEL_ID) {
120 /* We just found the matching model, so no point continuing the search */
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/model/
H A Dstatedata.c12 #include <mode/model/statedata.h>
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/
H A Dbenchmark_overflowHandler.h19 #include <model/statedata.h>
/seL4-l4v-10.1.1/seL4/include/arch/arm/armv/armv6/armv/
H A Dcontext_switch.h15 #include <mode/model/statedata.h>

Completed in 207 milliseconds

1234567891011>>