Module Wrapper

module Wrapper: sig .. end

The definition and implementation of a wrapper.

type pointer = Level.level -> Browser.Impl.state

A mapping from security level to a reactive system state

type wrapper_state = {

`p : pointer;`	`(*`	Points every level to the state of the original reactive system	`*)`
`ls : Level.level list;`	`(*`	List of levels on which the wrapper has still to produce output	`*)`
`all_ls : Level.level list;`	`(*`	All the levels at which the reactive system is running	`*)`

}

A type of the state of the wrapper

type waiting_w = wrapper_state

type running_w = wrapper_state

type state_w =

`\|`	`Waiting_w of waiting_w`
`\|`	`Running_w of running_w`

val start_w : state_w

An initial state of the wrapper.

Internal wrapper functions

exception WrongStateInUpdate

val update_pointer : Level.level -> pointer -> Browser.Impl.input_event -> pointer

update_pointer lev p ie if p lev is a waiting state, then updates the pointer p with the new state upon consuming the input ie. Otherwise return p.

val update_pointers : Level.level list ->
       pointer -> Browser.Impl.input_event -> pointer

update_pointers levs p ie at all the levels in levs moves the pointer p to the producer state corresponding to comsuming input ie. At all these levels the pointer must be in a waiting state.

val upper_acc : Level.level list -> input_event -> Level.level list -> Level.level list

val upper : Level.level list -> Browser.Impl.input_event -> Level.level list

upper levs ie defines a list of upper security levels for input event ie from the list of all levels levs.

exception WrongStateInGetOutput

val get_output : pointer -> Browser.Impl.input_event -> Browser.Impl.output_event list

get_output p ie produces output of the copy at level label_input ie on input ie. The current state of this copy should be a waiting state.

val filter_outputs_acc : output_event list ->
       Level.level ->
       Level.level list -> output_event list -> output_event list

filter_outputs_acc os lev new_add_levs acc is an auxiliary function for filter_output.

val filter_outputs : Browser.Impl.output_event list ->
       Level.level -> Level.level list -> Browser.Impl.output_event list

filter_outputs os lev new_add_levs filters list of outputs os leaving only those that are at level lev and higher. Also leaves those output events that are at level from the new list of levels new_add_levs.

val find_new_levels : Level.level list -> Level.level list -> Level.level list -> Level.level list

find_new_levels all_ls ls new_ls finds levels in the list of levels ls that are not in the list all_ls and put them in a list new_ls.

val make_new_copies : Level.level list -> Level.level -> pointer -> pointer

make_new_copies ls lev p makes copies of a state p lev and for every level l in a list ls defines p l := p lev.

val filter_one_output : Browser.Impl.output_event ->
       Level.level -> Level.level list -> Browser.Impl.output_event list

filter_one_output oe run_lev levs returns a list containing oe if the level of oe is run_lev or if it's higher than run_lev and is not in the list of currently running levels levs. Otherwise returns an empty list.

val filter_outputs_one_level_acc : Browser.Impl.output_event list ->
       Level.level ->
       Level.level list ->
       Browser.Impl.output_event list -> Browser.Impl.output_event list

An auxiliary function for a function filter_outputs_one_level oes run_lev levs.

val filter_outputs_one_level : Browser.Impl.output_event list ->
       Level.level -> Level.level list -> Browser.Impl.output_event list

filter_outputs_one_level oes run_lev levs filters outputs oes leaving only those that are at level run_lev.

Top-level wrapper functionality

val receive_w : Browser.Impl.input_event ->
       waiting_w -> state_w * Browser.Impl.output_event list

receive_w ie w respond to an incoming event ie while being in a waiting state w. The result is a new state and an output_event list.

val continue_w : running_w -> state_w * Browser.Impl.output_event list

continue_w r advance the wrapper state with one step from the running state r. Returns a new state and a list of output_event.