nettle-frp-0.1: FRP for controlling networks of OpenFlow switches.




Packet predicates and match semantics

class Logic m p whereSource

Type class for pairs of types where one type is a set of structures, and the other is a set of predicates over these structures, and for which there exists a relations of satisfaction.


holds :: m -> p -> BoolSource

(|-) :: Logic m p => m -> p -> BoolSource

A synonym for holds

data PacketPredicate Source

Packet Predicates Note that values of this data type should NOT be constructed using the constructors of this data type, but rather through the functions defined below. The functions below maintain this data type's invariants, whereas these constructors do not.

type Clause = [Literal]Source

A clause is a list of literals. A packet satisfies a clause if it satisfies all the literals in the clause. From this, it follows that any packet satisfies an empty clause; i.e. the empty clause is equivalent to True.

type Literal = PacketPredicateSource

A literal is any packet predicate except those formed using conjunction or disjunction. The type synonym does not enforce this constraint - we just use it as a reminder of the intent.

satisfies :: (PortID, EthernetFrame) -> PacketPredicate -> BoolSource

This function defines when an incoming packet (as received by a switch) satisfies a given packet predicate.

clauses :: PacketPredicate -> [Clause]Source

Computes the clauses for a packet predicate; assumes the data type invariants hold. A packet satisfies a list of clauses if it satisfies some clause in the list. From this it follows that no packet satisfies the empty list of clauses. I.e. the empty list of clauses is equivalent to False.

overlaps :: PacketPredicate -> PacketPredicate -> BoolSource

With the above, we can now calculate whether two packet predicates overlap, that is, when their intersection is non-empty.

Commonly occurring packet predicates.

dns :: PacketPredicateSource

Commonly occurring packet predicates.

Packet predicates and matches for this version

fromMatch :: Match -> PacketPredicateSource

Calculates a packet predicate that matches the same in-packets as the given match.

toMatches :: PacketPredicate -> Maybe [Match]Source

The disjunction of (toMatches pred) matches the same set of packets as the packet predicate pred does.