Quelle OpenFlow_Action.thy Sprache: Isabelle

theory OpenFlow_Action
imports
OpenFlow_Matches
begin

(* Beware the differences between Actions and Instructions. OF1.0 doesn't support the former and they're thus not modelled here. *)

(* OF1.0 says actions are a list and executed in-order, OF1.5 has two things: an action set with fixed order in 5.6 and an action list.
So\<dots> list. *)

(* Just those which we need(ed). *)
datatype of_action = Forward (oiface_sel: string) | ModifyField_l2dst "48 word"
(* Note that the 1.0 is not entirely clear that there's no drop action. 1.5 clarifies that this is represented by and empty instruction/action set. *)

(* So each flow entry has a list of these. Semantics\<dots> The actions are executed in order, but the order of the side-effects is not defined. *)
fun of_action_semantics where
"of_action_semantics p [] = {}" |
"of_action_semantics p (a#as) = (case a of
Forward i → insert (i,p) (of_action_semantics p as) |
ModifyField_l2dst a → of_action_semantics (p(p_l2dst := a)) as)"

value "of_action_semantics p []" (* Drop *)
value "of_action_semantics p [ModifyField_l2dst 66, Forward ''oif'']" (* set mac and send *)

end

Messung
C	H	Z	G
88	96	100	94

¤ Dauer der Verarbeitung: 0.1 Sekunden ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

Cephes Mathematical Library

Vienna Development Method

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 und die Messung sind noch experimentell.