rtedef

package
v0.0.0-...-8c93b70 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Sep 24, 2024 License: MIT Imports: 6 Imported by: 6

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func ConvertSTExpressionForPolicy 

func ConvertSTExpressionForPolicy(il InterfaceList, varNames []string, removeVarNames bool, expr stconverter.STExpression) stconverter.STExpression

ConvertSTExpressionForPolicy will remove from a single STExpression all instances of vars located in []varNames if acceptableNames == false a == input b == output "a" becomes "a" "b" becomes "true" (technically becomes "true or not true") "a and b" becomes "a" "func(a, b)" becomes "func(a, true)" "!b" becomes "true" (technically becomes "not(true or not true)") TODO: a transition based only on time becomes nil?

func DeepGetValues 

func DeepGetValues(expr stconverter.STExpression) []string

DeepGetValues recursively gets all values from a given stconverter.STExpression

func FBECCGuardToSTExpression 

func FBECCGuardToSTExpression(pName, guard string) ([]stconverter.STInstruction, *stconverter.STParseError)

FBECCGuardToSTExpression converts a given FB's guard into a STExpression parsetree

func STMakeSolutionAssignments 

func STMakeSolutionAssignments(soln stconverter.STExpression) []stconverter.STExpression

STMakeSolutionAssignments will convert a comparison stExpression into an assignment that meets the comparison The top level should be one of the following if VARIABLE ONLY, return VARIABLE = 1 if NOT(VARIABLE) ONLY, return VARIABLE = 0 if VARIABLE == EXPRESSION, return VARIABLE = EXPRESSION if VARIABLE > EXPRESSION, return VARIABLE = EXPRESSION + 1 if VARIABLE >= EXPRESSION, return VARIABLE = EXPRESSION if VARIABLE < EXPRESSION, return VARIABLE = EXPRESSION - 1 if VARIABLE <= EXPRESSION, return VARIABLE = EXPRESSION if VARIABLE != EXPRESSION, return VARIABLE = EXPRESSION + 1 otherwise, return nil (can't solve)

func SolveSTExpression 

func SolveSTExpression(il InterfaceList, inputPolicy bool, problemTransition PSTTransition, solutionTransition stconverter.STExpression) []stconverter.STExpression

SolveSTExpression will solve simple STExpressions It will project the solutionTransition onto the problemTransition Then, it will use the resulting transition with STMakeSolutionAssignments to convert the comparison into an assignment

func SplitExpressionsOnOr 

func SplitExpressionsOnOr(expr stconverter.STExpression) []stconverter.STExpression

SplitExpressionsOnOr will take a given STExpression and return a slice of STExpressions which are split over the "or" operators, e.g. [a] should become [a] [or a b] should become [a] [b] [or a [b and c]] should become [a] [b and c] [[a or b] and [c or d]] should become [a and c] [a and d] [b and c] [b and d]

func VariablesContain 

func VariablesContain(vars []Variable, name string) bool

VariablesContain returns true if a list of variables contains a given name

Types

type EnforcedFunction 

type EnforcedFunction struct {
	Name string `xml:"Name,attr"`

	InterfaceList

	Policies []Policy `xml:"Policy"`
}

An EnforcedFunction is what we're here for, it's what we're going to wrap with our policies!

func NewEnforcedFunction 

func NewEnforcedFunction(name string) EnforcedFunction

NewEnforcedFunction creates a new EnforcedFunction struct

func (*EnforcedFunction) AddIO 

func (f *EnforcedFunction) AddIO(isInput bool, intNames []string, typ string, size string, initialValue string) error

AddIO adds the provided IO to a given EnforcedFunction, while checking to make sure that each name is unique in the interface

func (*EnforcedFunction) AddPolicy 

func (f *EnforcedFunction) AddPolicy(name string)

AddPolicy adds a Policy to an EnforcedFunction

func (EnforcedFunction) PolicyProduct 

func (ef EnforcedFunction) PolicyProduct(polA Policy, polB Policy) (Policy, error)

PolicyProduct takes the product as defined by the EMSOFT '17 paper of two policies in an EnforcedFunction

Given two discrete TAs A1 = (L1 , l01 , lv1 , Σ1 , V1 , ∆1 , F1 ) and A2 = (L2 , l02 , lv2 , Σ2 , V2 , ∆2 , F2 ) with disjoint sets of integer clocks, their product is the DTA A1 × A2 A = (L, l0 , lv , Σ, V , ∆, F ) where L = L1 × L2 , l0 = (l01 , l02 ), lv = (lv1 , lv2 ), V = V1 ∪ V2 , F = F1 × F2 , and ∆ ⊆ L × G(V ) × R × Σ × L is the transition relation, with ((l1 , l2 ), g1 ∧ g2 , R1 ∪ R2 , a, (l1' , l2' )) ∈ ∆ if (l1 , g1 , R1 , a, l1' ) ∈ ∆1 and (l2 , g2 , R2 , a, l2' ) ∈ ∆2 . In the product DTA, all locations in (L1 × lv2 ) ∪ (lv1 × L2 ) are trap locations, and all the outgoing transitions for these locations can be replaced with self loops. We consider merging all the trap locations into a single location lv where any outgoing transition from any location in L \ (L1 × lv2 ) ∪ (lv1 × L2 ) to a location in (L1 × lv2 ) ∪ (lv1 × L2 ) goes to lv instead.

The product of DTAs is useful when we want to enforce multiple properties. Given two determin- istic and complete DTAs A1 and A2 the DTA A obtained by computing their product recognizes the language L(A1) ∩ L(A2), and is also deterministic and complete.

type InterfaceList 

type InterfaceList struct {
	InputVars  []Variable `xml:"Interface>Input"`
	OutputVars []Variable `xml:"Interface>Output"`
}

InterfaceList stores the IO

func (InterfaceList) HasIONamed 

func (il InterfaceList) HasIONamed(input bool, s string) bool

HasIONamed will check a given InterfaceList to see if it has an output of that name

type PEnforcer 

type PEnforcer struct {
	Name         string
	OutputPolicy PEnforcerPolicy
	InputPolicy  PEnforcerPolicy
	// contains filtered or unexported fields
}

A PEnforcer will store a given input and output policy and can derive the enforcers required to uphold them

func MakePEnforcer 

func MakePEnforcer(il InterfaceList, p Policy) (*PEnforcer, error)

MakePEnforcer will convert a given policy to an enforcer for that policy

func (*PEnforcer) ReturnManualRecovery 

func (enf *PEnforcer) ReturnManualRecovery(tr PSTTransition, inputPolicy bool) STExpressionSolution

ReturnManualRecovery will solve a given transition with specified recovery actions

func (*PEnforcer) SolveViolationTransition 

func (enf *PEnforcer) SolveViolationTransition(tr PSTTransition, inputPolicy bool) STExpressionSolution

SolveViolationTransition will attempt to solve a given transition TODO: consider where people have been too explicit with their time variables, and have got non-violating time-based transitions 1. Check to see if there is a non-violating transition with an equivalent guard to the violating transition 2. Select first solution

type PEnforcerPolicy 

type PEnforcerPolicy struct {
	InternalVars []Variable
	States       []PState
	Transitions  []PSTTransition
}

A PEnforcerPolicy is what goes inside a PEnforcer, it is derived from a Policy

func DeriveInputEnforcerPolicy 

func DeriveInputEnforcerPolicy(il InterfaceList, outPol PEnforcerPolicy) PEnforcerPolicy

DeriveInputEnforcerPolicy will derive an Input Policy from a given Output Policy

func (PEnforcerPolicy) DoesExpressionInvolveTime 

func (pol PEnforcerPolicy) DoesExpressionInvolveTime(expr stconverter.STExpression) bool

DoesExpressionInvolveTime returns true if a given expression uses time

func (PEnforcerPolicy) GetDTimers 

func (pol PEnforcerPolicy) GetDTimers() []Variable

GetDTimers returns all DTIMERS in a PEnforcerPolicy

func (PEnforcerPolicy) GetNonViolationTransitions 

func (pol PEnforcerPolicy) GetNonViolationTransitions() []PSTTransition

GetNonViolationTransitions returns a slice of all transitions in this PEnforcerPolicy that have their destinations not set to "violation", ie. are not violation transitions

func (PEnforcerPolicy) GetNonViolationTransitionsForSource 

func (pol PEnforcerPolicy) GetNonViolationTransitionsForSource(src string) []PSTTransition

GetNonViolationTransitionsForSource returns a slice of all transitions in this PEnforcerPolicy which have a source as "src" and have their destinations not set to "violation", ie. are not violation transitions

func (PEnforcerPolicy) GetTransitionsForSource 

func (pol PEnforcerPolicy) GetTransitionsForSource(src string) []PSTTransition

GetTransitionsForSource returns a slice of all transitions in this PEnforcerPolicy which have a source as "src"

func (PEnforcerPolicy) GetViolationTransitions 

func (pol PEnforcerPolicy) GetViolationTransitions() []PSTTransition

GetViolationTransitions returns a slice of all transitions in this PEnforcerPolicy that have their destinations set to "violation", ie. are violation transitions

func (*PEnforcerPolicy) RemoveAlwaysTrueTransitions 

func (pol *PEnforcerPolicy) RemoveAlwaysTrueTransitions()

RemoveAlwaysTrueTransitions will do a search through a policies transitions and remove any that are just "true"

func (*PEnforcerPolicy) RemoveDuplicateTransitions 

func (pol *PEnforcerPolicy) RemoveDuplicateTransitions()

RemoveDuplicateTransitions will do a search through a policies transitions and remove any that are simple duplicates (i.e. every field the same and in the same order).

func (*PEnforcerPolicy) RemoveNilTransitions 

func (pol *PEnforcerPolicy) RemoveNilTransitions()

RemoveNilTransitions will do a search through a policies transitions and remove any that have nil guards

type PExpression 

type PExpression struct {
	VarName string
	Value   string
}

PExpression is used to assign a var a value based on a PTransitions

type PSTTransition 

type PSTTransition struct {
	PTransition
	STGuard stconverter.STExpression
}

PSTTransition is a container struct for a PTransition and its ST translated guard

func ConvertPSTTransitionForInputPolicy 

func ConvertPSTTransitionForInputPolicy(il InterfaceList, inputPolicy bool, outpTrans PSTTransition) PSTTransition

ConvertPSTTransitionForInputPolicy will convert a single PSTTransition from an Output Policy to its Input Policy Deriviation

func SplitPSTTransitions 

func SplitPSTTransitions(cTrans []PSTTransition) []PSTTransition

SplitPSTTransitions will take a slice of PSTTRansitions and then split transitions which have OR clauses into multiple transitions it relies on the SplitExpressionsOnOr function below

type PState 

type PState string

PState is a state in the policy specification of an enforcerFB

func (PState) Name 

func (p PState) Name() string

Name returns the name of a PState

type PTransition 

type PTransition struct {
	Source      PState
	Destination PState
	Condition   string
	Expressions []PExpression //output expressions associated with this transition
	Recover     []PExpression
}

PTransition is a transition between PState in a Policy (mealy machine transitions)

type Policy 

type Policy struct {
	Name         string        `xml:"Name,attr"`
	InternalVars []Variable    `xml:"InternalVars>VarDeclaration,omitempty"`
	States       []PState      `xml:"Machine>PState"`
	Transitions  []PTransition `xml:"Machine>PTransition,omitempty"`
}

Policy stores a policy, i.e. the vars that must be kept

func (*Policy) AddDataInternals 

func (efb *Policy) AddDataInternals(intNames []string, typ string, isConstant bool, size string, initialValue string) *Policy

AddDataInternals adds data internals to a efb, and adds the InternalVars section if it is nil

func (*Policy) AddState 

func (efb *Policy) AddState(name string) error

AddState adds a state to a bfb

func (*Policy) AddTransition 

func (efb *Policy) AddTransition(source string, dest string, cond string, expressions []PExpression, recoveries []PExpression) error

AddTransition adds a state transition to a bfb

func (*Policy) GetPSTTransitions 

func (p *Policy) GetPSTTransitions() ([]PSTTransition, error)

GetPSTTransitions will convert all internal PTransitions into PSTTransitions (i.e. PTransitions with a ST symbolic tree condition)

func (*Policy) SortTransitionsViolationsToEnd 

func (p *Policy) SortTransitionsViolationsToEnd()

SortTransitionsViolationsToEnd decreases the priority of all violation transitions but otherwise keeps them in the same order

type STExpressionSolution 

type STExpressionSolution struct {
	Expressions []stconverter.STExpression
	Comment     string
}

STExpressionSolution stores a solution to a violation transition

type Variable 

type Variable struct {
	Name         string `xml:"Name,attr"`
	Type         string `xml:"Type,attr"`
	Constant     bool   `xml:"Constant,attr"`
	ArraySize    string `xml:"ArraySize,attr,omitempty"`
	InitialValue string `xml:"InitialValue,attr,omitempty"`
	Comment      string `xml:"Comment,attr"`
}

A Variable is used to store I/O or internal var data

func (Variable) GetInitialArray 

func (v Variable) GetInitialArray() []string

GetInitialArray returns a formatted initial array if there is one to do so

func (Variable) IsDTimer 

func (v Variable) IsDTimer() bool

IsDTimer returns true if DTimer

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.