Pushlogic originally generated its own native object-level bytecode. This was considered the reference standard for code reflection. Anything that generated this form of code could particpate in the system.
Now (2008), the Pushlogic compiler also generates .net IL code. The code can be checked whether conformant to one or more checkablity profiles and the domain manager will reject bundles that are outside its supported set of checkability profiles.
Pushlogic native object level is considered the primary form of represenation. It exists in bytecode and XML forms.
The XML schema for Pushlogic code reflection is as follows. A separate schema is used for data reflection via the tuplecore (todo: where is it listed?).
<?xml version="1.0" encoding="UTF-8"?> <xs:schema
xmlns:xs="http://www.w3.org/2001/XMLSchema" elementFormDefault="qualified">
<xs:element name="bundle">
<xs:complexType>
<xs:sequence>
<xs:element maxOccurs="unbounded" ref="PK_subxw"/>
<xs:element maxOccurs="unbounded" ref="PK_domain"/>
<xs:element maxOccurs="unbounded" ref="PK_rule"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="PK_subxw">
<xs:complexType mixed="true">
<xs:sequence>
<xs:element minOccurs="0" maxOccurs="unbounded" ref="PK_fieldr"/>
</xs:sequence>
<xs:attribute name="no" use="required" type="xs:integer"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_fieldr">
<xs:complexType>
<xs:choice>
<xs:element ref="PK_fielda"/>
<xs:element ref="PK_tup"/>
</xs:choice>
<xs:attribute name="arg1s" use="required" type="xs:NCName"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_domain">
<xs:complexType>
<xs:sequence>
<xs:element minOccurs="0" maxOccurs="unbounded" ref="PK_s"/>
<xs:element minOccurs="0" ref="PK_ellipsis"/>
<xs:element ref="PK_fieldd"/>
</xs:sequence>
<xs:attribute name="mode" use="required" type="xs:NCName"/>
<xs:attribute name="safecount" use="required" type="xs:integer"/>
<xs:attribute name="spare" use="required" type="xs:NCName"/>
<xs:attribute name="unsafecount" use="required" type="xs:integer"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_ellipsis">
<xs:complexType/>
</xs:element>
<xs:element name="PK_fieldd">
<xs:complexType>
<xs:choice>
<xs:element ref="PK_fielda"/>
<xs:element ref="PK_tup"/>
</xs:choice>
<xs:attribute name="arg1s" use="required" type="xs:NCName"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_rule">
<xs:complexType>
<xs:sequence>
<xs:element ref="PK_fieldw"/>
<xs:choice>
<xs:element ref="PK_query"/>
<xs:element ref="PK_s"/>
</xs:choice>
<xs:element maxOccurs="unbounded" ref="PK_skip"/>
</xs:sequence>
<xs:attribute name="timer" use="required" type="xs:integer"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_fieldw">
<xs:complexType>
<xs:sequence>
<xs:element ref="PK_fielda"/>
</xs:sequence>
<xs:attribute name="arg1s" use="required" type="xs:NCName"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_tup">
<xs:complexType>
<xs:attribute name="arg1tup" use="required" type="xs:NCName"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_fielda">
<xs:complexType>
<xs:sequence>
<xs:element ref="PK_tup"/>
</xs:sequence>
<xs:attribute name="arg1s" use="required" type="xs:NCName"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_s">
<xs:complexType>
<xs:attribute name="arg1s" use="required"/>
</xs:complexType>
</xs:element>
<xs:element name="PK_query">
<xs:complexType>
<xs:sequence>
<xs:choice minOccurs="0" maxOccurs="unbounded">
<xs:element ref="PK_deqd"/>
<xs:element ref="PK_query"/>
<xs:element ref="PK_s"/>
<xs:element ref="PK_subxr"/>
<xs:element ref="PK_and"/>
</xs:choice>
<xs:element minOccurs="0" ref="PK_backstop"/>
<xs:element ref="PK_skip"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="PK_and">
<xs:complexType>
<xs:sequence>
<xs:choice maxOccurs="unbounded">
<xs:element ref="PK_deqd"/>
<xs:element ref="PK_subxr"/>
</xs:choice>
<xs:element ref="PK_skip"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="PK_backstop">
<xs:complexType/>
</xs:element>
<xs:element name="PK_skip">
<xs:complexType/>
</xs:element>
<xs:element name="PK_deqd">
<xs:complexType>
<xs:sequence>
<xs:element minOccurs="0" maxOccurs="unbounded" ref="PK_query"/>
<xs:element minOccurs="0" ref="PK_subxr"/>
<xs:element ref="PK_s"/>
<xs:element ref="PK_skip"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="PK_subxr" type="xs:NMTOKEN"/>
</xs:schema>
This schema is partial since it does not currently list all of the diadic operators. The PK_skip statement is shown instead of the pushback info in this version.
The bytecode is defined in this table:
Pushlogic Byte Code Descriptions : DRAFT. For the bytecode representation, self-describing args preceed the bytecode and fixed-field args follow the byte code. For the XML representation, self-describing args are included as sub-elements of the element and the fixed-field args are put as attributes. OPERATORS -- CODE PK_and 2 Logical and function. Three stack args : left, right and pushback info. No postfix attributes. -- CODE PK_or 3 Logical or function. Three stack args : left, right and pushback info. No postfix attributes. -- CODE PK_not 4 Logical not function One stack arg. No postfix attributes. -- CODE PK_inv 5 Bitwise complement. One stack arg. No postfix attributes. -- CODE PK_xor 6 Logical xor function. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_divide 32 Division operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_mod 33 Modulus operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_fqgt 34 Four quadrant greater than operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_multiply 35 Multiplication operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_query 14 Conditional expression operator. Four stack args: guard, true-exp, false-exp, pushback info. No postfix args. --- CODE PK_deqd 15 Equality comparison operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_dgtd 16 Greater than comparison operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_dged 17 Greater than or equals comparison operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_plus 20 Addition operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_minus 21 Subtraction operator. Three stack args : left, right and pushback info. No postfix attributes. --- CODE PK_tup 22 Reference to a tuple in the current domain of participation - sometimes currently used instead of localroot. No stack args. One postfix attribute: the tuple name. CONSTANT VALUES CODE PK_s 1 Defines a string constant No stack args. One postfix attribute: the string itself. --- CODE PK_backstop 19 A constant value which when assigned does not change the current value. No stack args. No postfix args. --- CODE PK_int 25 No stack args. In bytecode, a representation of integers in base 256. In XML, integer elements appear directly. --- CODE PK_nint 26 No stack args. In bytecode, a representation of integers in base ???. In XML, integer elements appear directly. --- CODE PK_ellipsis 28 A constant value which denotes other possible values in a domain declaration. No stack args. No postfix args. --- CODE PK_range 29 Declares a subrange of the integers. Two stack args: from and to inclusively. No postfix args. --- TOP LEVEL ITEMS -- CODE PK_rule 7 Defines an executable rule Six stack args are left-hand side tuple, left-hand field, right-hand side, pushback, spare and spare. In XML form, the left-hand side tuple and field are combined and use a single element. One postfix attribute: nominally called timeout but currently unused. -- CODE PK_subxw 8 Define a subexpression. One stack arg: any expression One postfix attribute: the subx number. --- CODE PK_subxr 9 Read a subx defined by subxw. Zero stack args. One postfix attribute: the subx number. CODE PK_domain 30 Declares the range of values for a field. Stack args: the safe values followed by the unsafe values. Three postfix args: type, safe values, unsafe value. ---- CODE PK_safetylive 24 // not used now An Oldform ? ---- CODE PK_sl 40 Safety/live rule definition. Three stack args : guard, true/false and message. No postfix attributes. The middle value is true for a safety rule and false for a live rule. The message should be reported if the rule fails. Fairness constraints are to be added! ---- CODE PK_fieldl 41 not used anymore? FIELD AND TUPLE ACCESS --- CODE PK_localroot 13 Explicit name for the local root tuple - sometimes currently omitted by implication. No stack args. No postfix args. --- CODE PK_uri 27 Reference to a tuple on another execution platform. No stack args. One postfix attribute: the uri. ---- CODE PK_fielda 23 A field reference where the field contains a tuple. One stack arg: a tuple. One postfix arg: the field name. --- CODE PK_fieldw 10 A field reference for writing. One stack arg: a tuple. One postfix arg: the field name to be written. --- CODE PK_fieldr 18 A field reference for reading. One stack arg: a tuple. One postfix arg: the field name to be read. ---- CODE PK_fieldlk 39 A field declaration where the field will be a lock. One stack arg: a tuple that will contain the field. One postfix arg: the field name. --- CODE PK_fieldd 36 A field declaration. One stack arg: a tuple that will contain the field. One postfix arg: the field name. ---- MISCELLANEOUS CODE PK_eventr 42 event read: pushlogic interepreter internal use only. Does not appear in bytecode currently - inferred by bcload. --- CODE PK_pbind 37 Pushback info. ??? currently being changed sligthtly --- CODE PK_pbval 38 Pushback info. ??? currently being changed sligthtly --- CODE PK_meta 11 Not used. --- CODE PK_skip 12 A nop. No stack args. No postfix args. ---- CODE PK_eob 31 End of bundle marker - not used in XML form. No stack args. No postfix args. EOFThe XML schema essentially follows the bytecode, in that a very simple tree walker is all that is needed to convert XML form to bytecode. The current pushlogic interpreter indeed converts it in this way.
Pushlogic has three forms of representation: source, canned object and re-hydrated object. In this section we give the semantics of re-hydrated object, which is regarded as the primary form of Push Logic. It is actually a bytecode suitable for automated checking, distribution and loading into an execution platform (bytecode interpreter).4.1
A Pushlogic program, at the object level, is a set of rules known as a `bundle'. Pushlogic programs are aggregated into a domain of participation by disregarding bundle boundaries and forming the union set of rules, but a bundle may not be admitted if automated formal tests fail for any rule within it. These tests are given below. Each one is called a `constraint'. A race can arise if an attempt is made to load a pair of incompatible bundles at once: the system will accept only the rules from the first bundle.
Pushlogic object rules have three forms: executable, liveness and safety. The source compiler can convert more complex temporal constraints into a conjunction of live and safety checks for the object form to handle. Liveness and safety rules are assertions to be checked by a model checker invoked by the loader. The loader also has certain built-in constraints, described below, that require model checking. (The model checker can be run as a network service or as a process on the target execution platform.) The combination of the current bundle and all other rules in the domain of participation is model checked. If all assertions still hold, then the new bundle is acceptable to the domain and becomes part of it. Execution of its executable rules is then allowed.
Pushlogic atomic object expressions are the constant values (strings,
integers and bottom (
)) and the values of fields.
More complex expressions are built up using operators. The operators are any deterministic, referentially-transparent functions, including the normal Boolean connectives and the conditional expression construct (query-colon). The full core set of operators found in Java and C++ is supported, along with string catenation. Function calls could be provided for brevity, but these are currently fully inlined by the compiler and so do not appear in the object code.
Expressions are either level or event expressions. A level expression is a function of state whereas an event expression will only have a non-null value momentarily.
Arithmetic and comparison operators are provided using the
normal coercion rules that allow strings and integers to be
interchanged, as found in languages such as Perl. is
represented with a unique byte code that is disjoint from any string:
does not need to be explicitly written in the Pushlogic
source level.
A full list of operators should be given here. Note that string cat uses
dot and 
is xor.
A FQGT operator is provided that performs a comparison in the style of greater-than but with the assumption that a pair of integers in a adjacent quadrants of the number space have not lapped each other. Example needed here ...
Our current, main Pushlogic implementation is part of a distributed tuple space platform and hence variables are called fields. Most fields are either events or range over the constant string/integer values defined above. Apart from strings, integers and events, the tuple space platform supports some other types, including level, primary key, credit, URI and so on. Their definition is beyond the scope of this document and so only mentioned in passing.
A tuple is a collection of fields, each named with a tag string. A field may contain a nested tuple.
Every tuple has a field called `level (i.e. the tag string for that
field is `level'). It contains a negative integer.
All fields and tuples are part of a global shared address space, and in principal, can be accessed from any bundle. However, the concepts of domain, device, pebble and bundle each impose overlays of name aliasing and access control on the global space.
Certain tuples are associated with the current DoP, certain with the current device or execution platform and certain exist only for private, local access by the current bundle. Like a bundle, a pebble also possesses a set of associated local fields, but these are not private: indeed they are used as shared variables for communication with the Pebble.
As a coding convention, users of Pushlogic are invited to use first-letter capitalisation for then names of fields that contain tuples and lower case for fields that are variables.
Fields that are local to the current bundle are declared with the keyword `local'. Fields that are shared and provide input or output to the current bundle are declared with the keywords `input', `inout' or `output'. Actually, at object level, the keywords are replaced with Pushlogic bytecodes.
The built in types, such as `lock', `bool' or `fuse' can be used at source level as a short hand to declare local fields. For example, the following two lines show equivalent ways of defining booleans.
local var1, var2 : bool;
bool var3, var4;
The definition of fields and tuples is identical at source level and object level and is unchanged by the compiler.
When a field is declared, a range of values for it may also be declared. If the range is to be used frequently, it can be named and represented as a `type' and then refered to by its name. The range is denotation of a list of constant strings, but integer subranges can be used to specifiy parts of this list.
The range of values is partitioned into safe and unsafe values. The the list of safe values is definitive, whereas code should operate correctly and all assertions pass if further unsafe strings or integers occur during run time. This supports dynamic system extensibility. The elipsis construct is allowed in list of unsafe value at the the pushlogic source level, but serves only to alter behaviour with respect to compile-time warnings.
One of the safe values, the first listed in any list, is known as the nominal starting value for that field, and can be used as such in offline checks that involve reachable state analysis.
When a bundle (or pebble) is introduced to a DoP, if the nominal starting value of any of the the newly created fields associated with the new bundle (or pebble) is inconsistent with extant domain values, fields may be set to any value that makes the rules consistent, but with priority being given first to nominal starting values, then to other safe values, then to listed unsafe values.
If insertion of a new bundle (or pebble) into a DoP would immediately cause a pushback inside the domain, this should perhaps be flagged at a meta-level to the operative attempting the insertion.
Expressions are either level or event expressions. It is possible to define the distinction in a syntax-directed way, as given shortly. However, the current and preferred implementation is not to rely on syntax but to use the elaboration rules in the compiler to determine whether a given expression is acceptable in a given context. The rules deny the conjunction of events from separate sources and require that all code reaches closure under repeated symbolic elaboration (§5.14.2). The elaboration rules offer a richer language since the syntax-directed form cannot easily encompass concepts of an differentiator enclosed in an integrator.
The following rules would be broadly sufficient to distinguish level expressions from event expressions, but they are intended as a guide to programmers and are not a definition.
A level expression is essentially an expression with no leaf variables of type `event' and which does not contain the differentiation operator. It maintains its value unless any of the supporting variables changes their current value (their level in hardware terms).
An event expression is a function of one or more variables of type `event' or which contain the differentiation operator. Not all operators support event arguments: those that do are conjunction, disjunction and conditional expression (query-colon construct); negation of events is forbidden. Disjunction of event expressions (logical OR) is always allowed but conjunction requires that both arguments stem from a single external event delivered to the current bundle. The basis of this is that simultaneous delivery of external events is not meaningful.
The `always' assertion asserts that a condition must always hold and its argument must be a level expression. The `never' and `live' assertions may apply to either type of expression.
Further temporal logic operators, such as `until' and ` w-until' and general CTL expressions, are not currently supported, but will have the requirements on their arguments that would arise from decomposition into safety and liveness form.
is a field (a scalar variable name) in a global name space
and 
is a Pushlogic object expression and 
is compensation information
that asists in reversing the operation of the rule. This information
also identifies certain of the expression support (i.e. certain of the free variables
occuring in ) as the sensitive parents of the rule.
All pushlogic rules, at the object level, are composed in parallel and execute simultaneously.
D1: Rule Execution: The reference execution model for an executable Pushlogic rule is that all subexpressions occurring in the expression are re-evaluated whenever there are changes to any of their support. Likewise, changes to the result of the top expression become scheduled as updates to the assigned field. Updates are gated, by which we mean that all updates to fields held on the same execution platform as the Pushlogic that arise owing to a single event are batched and made at once (atomically). Further changes arising from a batch of gated updates are collected and deferred to the next batch.
An event nominally holds for one gated cycle. All event fields are re-set to the null string after the cycle where they were processed.
A Pushlogic rule is to be thought of as holding at all times, except
when it is assigning 
, at which times the assigned field
retains its current value or is controlled by another rule. Push
Logic is designed such that each rule may also be interpreted as an
assertion about the current state of the assigned field and the
conjunction of all such assertions should hold at all times. However,
because fields may be held on physically separate devices, and Push
Logic interpreters interchange network messages when fields need to be
changed, this conjunction will not globally hold for brief periods
while network messages are in flight or during network disconnect.
The occurance of event expresions in executable rules is restricted
by the following schema. The executable rule must be factorisable into
one of three forms, where 
denotes an event expression, 
denotes a level expression, 
denotes a level variable and 
denotes
an event variable. The four forms are:
The second form is known as an 'emit' assignment (§5.10.1).
The third and fourth forms are known as integrations.
Local fields will not suffer unilateral changes: all changes will accrue from executable rules in the associated bundle.
When an executable rule makes a change to a field that fails (a failed update), the rule is obliged to compensate with corrective action. Otherwise, the rule could no longer be viewed also as a universally quantified assertion about the state of the domain. The update may fail straightaway or else the field may revert to some safe value after an interval of time. Either way, the system must perform a `pushback' after a failure. A `simple undo' involves changing a sensitive parent of the rule to a safe value that again makes the rule hold (when viewed as an assertion). An undo must also be performed by the rule if another rule or an external agent changes its driven field.
Push back information must be provided where there would otherwise be more than one possibility for compensating. If an external agent (or other rule) changes the value of the assigned field to one of its safe values, the push back indication uniquely identifies fields occurring in the associated expression that can be changed to make the rule hold. For information loosing operators, values must also be provided. For example, with logical not, no indication is required, because the new value is obvious at push back time. For comparison when pushed back so it holds, then it is sufficient to specify one operand to push back on, since it must be pushed back to the current value of the other operand. For comparison, when pushed back to false, a value and operand must be specified, since, in general, there are many possible vaues that will make a comparion fail. For conjunction, when pushed back to false, knowning which operand to push on is required, since either will do, whereas to push conjunction to hold may require both its arguments to be changed. For the conditional expression operator, the condition may have to be changed and also the value of that side of the operator may have to be changed.
The pushlogic source `cut' function, (or whatever it is currently called!) does not appear in the object code - it serves only to influence the push back information.
The complex undo is expanded at compile time using extensions of the fuse statement. No object-level representation is needed.
All communication between entities is through shared variables. (Multimedia is supported using the notion of third-party setup, where a field in a source pebble is set to the same value as a field in a sink pebble, where the value acts as a virtual circuit identifier).
Where a bundle alters the value of a field held on a remote resource, the run time system generates network traffic, such as a SOAP RPC [16]. Where a bundle is sensitive to changes on remote resources, it uses a soft-state registration protocol (a UDP version of UPnP's GENA) that causes it to receive notification of changes. An inout field may be set to one of its non-safe values by at most one bundle.4.2
Changes in local or remote field values are notified to the Pushlogic execution
engine because it registers for appropriate notification callbacks.
![\begin{displaymath}
v := [\![{ {exp} }]\!]_\sigma
\end{displaymath}](img15.png){kind=small}
Apart from embedded safety and liveness constraints coming from bundles, every DoP is subject to the following standing system constraints. A bundle cannot be loaded if it would violate any of these constraints.
PLC1: Level Ordering Constraint: For every rule, the level of the
assigned field must be less than any level found in the supporting
parents (free fields of) its assigned expression
Fields may be allocated new levels by the system as part of the process of loading a bundle. However, this is not always successful because a pair of rules in different bundles may have contradictory field level requirements. Where the fields are held on different execution platforms, a distributed algorithm may be run to establish their levels. If this constraint cannot be met, the bundle is not loaded.
The level ordering constraint does not apply to local variables, including lock or fuses or compiler-generated program counters.
PLC2: Consistency Constraint: A Pushlogic object expression may be
deterministically evaluated in an environment, 
, to produce a
string or else the special value bottom, . When a rule produces
, it has no affect on the assigned field:
![$\sigma[\perp/v] = \sigma$](img18.png){kind=small}
.
To ensure consistency (i.e. to avoid fighting between rules), all rules that assign a given field must evaluate to a common non-bottom value or bottom itself in all possible environments. Each rule of a new bundle is checked against the existing participating rules and the bundle is not loaded if any violates this condition.
PLC2b: No race hazards: Any program that contains a race of the nature shown in figure 4.1 will not unwind during compilation since the final result depends on the order of interleaving.
PLC3a: Safe Value Constraint A: A pair of bundles is incompatible if they disagree on their safe value declarations for any field.
PLC3b: Safe Value Constraint B: There must exist at least one setting of the fields such that all executable rules hold and all fields that have safe values defined are set to one of those safe values.
PLC3c: Safe Values Constraint C: The safe values of a field must be a subset of the safe values that any expression assigned to that field can safely generate, or else the expression must be able to safely generate bottom. By safely generate, we mean that the expression generates that value when all of its supporting fields are set to their safe values. This constraint ensures that when a pushback occurs, and an assigned value is set to one of its safe values, the assigned expressions can push back on their support, safely, so that the rule holds. (This constraint is stricly stronger than PLC3b ?).
PLC3d: Safe Live Insertion Constraint: An insertion into a DoP that causes an immediate pushback may be considered an error in some applications. At least a warning or deferral should be offered to the operative.
PLC4: Push Back Uniqueness: Only one possible pushback procedure
should be possible for each possible pushback circumstance. If there
is more than one, then the information is ambiguous. The
constraint implies that where a parent is shared between multiple
rules of a bundle there is just one change to the parent that is
acceptable with respect to this constraint for all rules sharing that
parent field. 4.3
D7: Undo Race Avoidance: Where an undo operates over the network between different execution platforms, a race can arise, where another independent change to the driven field has been performed by another rule or external agent. This normal course of events is illustrated in figure 4.2, whereas figure 4.3 shows the race condition. To overcome races, a simple undo ... TBD. Needs work.
Declarative programming languages aim to consist of a set of declarations that all hold at all times. On the other hand, many useful control sequences cannot be expressed entirely declaratively. For instance, when we press the `skip forward' key on a CD or DVD player, we expect it to jump to the next track or index point. When we press the button again, a new definition of 'next' now pertains and so the operation is not idempotent. Implementation of this feature requires both a differentiation to detect the active edge of the button push and an integration to accumulate the increment to the track number.
PLC5: Idempotency Constraint: Any Pushlogic program will result in no further output changes if `executed' more than once without unilateral (external) change of any field.
Idempotency is assured if every integration is uniquely associated
with a differentiation. In addition, an integration of the form
breaks the Level Ordering Constraint in that 
occurs
on both side of the rule and hence the level on both sides is equal.
The solution to this dichotomy is provided by the Gated Update mechanism.
The gated nature of updates to fields all held on a common platform allows that certain rule combinations to operate deterministically when they would not otherwise. Consider the following pair of rules where d1 is a tightly-coupled field:
The int-diff constraint provides that an infinite while loop wrapped around a parallel statement, that contains no internal waits, is not sensitive to the additional loops made by the thread.
PLC6a: Montonicity constraint: All rules must meet the other constraints with any amout of extension to the range of unsafe values in any field.
The constraints on allowable Pushlogic programs (union of unbundled rule bundles) have just been presented. These constraints can be checked without full possession of the Pushlogic object code. This could be very useful in large systems or where IP or policy needs to be protected. A summary form for a bundle may be defined that lists for each assign field the level constraints and the possibly assigned values. Where the Pushlogic Timer or other common resource is frequently depended on, then the summary can helpfully mention this explicitly. For instance, a set of different bundles might control a common field at different times of day and these would appear incompatible if time were ignored, but by including it in the summary, the bundles become compatible.
PLC6b: Montonicity constraint: Any bundle, whose assertion guarantees rest on the presence of other bundles that might become unloaded, is not allowed. (This is checked using a non-deterministic presence guard for each unloadable bundle by the domain manager).
PLC7: No oscillations constraint: Oscillation is created by inverting loops. Any bundle that contains an internal oscillating loop cannot be elaborated by the compiler and causes a compile-time error. When bundles are brought together with each other or world models any oscillators then formed are detected by the domain manager and the union is not allowed.
For example, the following two lines are inconsistent since they form an oscillator. If the lines are in the same bundle, a compile-time unwind fail error is flagged. If they are in different bundles but the variables are bound to form a distributed inverting loop then the oscillation error is flagged by the domain manager.
a := b; b := !a;
Many device control loops are oscillators, such as those used in thermostats. In order to implement these, the loop must be broken using a time delay at some point to regulate the maximum frequency of oscillation. For example:
with Timer#Countdown if (#atimer == 0)
{
#atimer := 1000; // Delay for one second
b_delayed = b;
}
a := b_delayed;
b := !a;
Resynchronisation Constraint: A liveness predicate expresses that two supposedly-coupled systems will eventually become re-synchronised after network distruption has finished.
A bundle may contain a number of safety or liveness assertions. These take expressions as arguments and the expressions have the form defined in §4.3.
Object-level safety and liveness assertions are checked by the Domain Manager at bundle load time. They are retained by the Domain Manager for further checking against newly arriving bundles. Monotonicity constraints imply they cannot be violated by bundle or pebble departure.