NB: There is a user manual for the source compiler in html on the website. This chapter discusses the source language per se, rather than how to compile it.
Although rules are frequently a useful way to express desired behaviour, many applications are most easily coded in an imperative programming style. Rather than expecting the user to manually convert his notions of application behaviour into Pushlogic object rules, a compiler for imperative-style expression of applications is used. We note that imperative programs deal essentially with sequential changes of state, whereas logical predicates over application programs deal in terms of the visible, accumulated results of these changes.
`Pushlogic Source' is a block-structured, imperative-like, programming language, but with no dynamic storage allocation and currently no arrays. It is less fundamental to our approach than the object form, because a variety of source forms could be envisaged that would generate compatible object for various niche applications. The Pushlogic constraints on a bundle are implemented at bundle load time, but, as far as possible, are also implemented by the compiler to give advanced warning.
The concrete syntax tree is following yacc file:
/*
* $Id: pushlogic.yy,v 1.35 2008/07/11 08:15:04 djg11 Exp $
*
* Bigtop.
# CBG Badger Tuplers Project
# University of Cambridge
# Computer Laboratory
# (C) 2004 David J Greaves
#
# Mostly Written Romsey - Dec 2004.
#
*
* Pushlogic Grammar
*/
%{
#include "cbglish.h"
#include <stdio.h>
#define PL_LINEPOINT(X) add_linepoint("pl_linepoint", X)
%}
%union {
builder *auxval;
}
%type <auxval> pl_assoclist pl_associtem bytecode
%type <auxval> pushl_decls prog module value value_list value_list_or_nil
%type <auxval> pushl_def pl_formals pl_actuals pl_formal pushl_defstyle
%type <auxval> pushl_statement pushl_statement_list case_item case_item_list pl_type
%type <auxval> pushl_statename pushl_statechartlist pushl_state pushl_stateitemlist pushl_stateitem pushl_statespec
%type <auxval> sd_id_comma_list pushl_field_decl pushl_macro_decl pushl_macro_decl_list pushl_field_decl_list
%type <auxval> exp exp1 exp2 exp3 exp4 exp5 exp6 exp7 exp8 exp9 exp10 exp11 exp12 exp12a exp13 exp13a
%type <auxval> string_option
%type <auxval> formal_comma_list exp_comma_list exp12_comma_list
%type <auxval> xml_file xml_element xml_element_list xml_att_list
%%
prog:
pushl_decls
{
builder *r = $1;
results = LISTCONS(r, results);
$$ = freverse(results);
}
;
bytecode:
/* nothing */ { $$ =
LISTEND(0);
}
| sd_string sd_number bytecode { $$ =
LISTCONS(TREE2("pl_stringtab", $1, $2), $3);
}
| sd_number bytecode { $$ =
LISTCONS(TREE1("pl_bytecode", $1), $2);
}
;
pushl_decls: /* nothing */ { $$ =
LISTEND(0);
}
| module pushl_decls { $$ =
LISTCONS($1, $2);
}
;
pushl_statement_list: /* nothing */ { $$ =
LISTEND(0);
}
| pushl_statement pushl_statement_list { $$ =
LISTCONS($1, $2);
}
;
/* A simple xml parser here for reading in compiled bundles and code reflected fragments */
xml_qbody: /* It would be better to handle this xmlq in the lexer ? */
sd_id xml_qbody
| sd_string xml_qbody
| ss_equals xml_qbody
| ss_minus xml_qbody
| ;
xml_element_list: ss_dltd ss_slash sd_id ss_dgtd { $$ =
LISTEND(0);
}
| xml_element xml_element_list { $$ =
LISTCONS($1, $2);
}
;
xml_att_list: { $$ =
LISTEND(0);
}
| sd_id ss_equals sd_string xml_att_list { $$ =
LISTCONS(TREE2("xml_att", $1, $3), $4);
}
;
xml_element:
ss_dltd sd_id xml_att_list ss_dgtd xml_element_list
{ $$ = TREE3("xml_element", $2, $3, $5); }
| ss_dltd sd_id xml_att_list ss_xml_singleton
{ $$ = TREE3("xml_element", $2, $3, LISTEND(0)); }
| sd_id { $$ = TREE1("xml_chars", $1); }
| sd_number { $$ = TREE1("xml_int", $1); }
;
xml_file:
ss_xmql xml_qbody ss_xmqr xml_file { $$ = $4; }
| xml_element { $$ = $1; }
;
module:
pushl_def pl_semicolon_opt { $$ = $1; }
| pushl_statement { $$ = $1; }
| ss_pling bytecode {
$$ = TREE1("pl_compiled_bundle", $2);
}
| ss_xmql xml_qbody ss_xmqr xml_file { $$ = TREE1("pl_xml", $4); }
;
pl_semicolon_opt: ss_semicolon | /* nothing */
;
pl_formals:
ss_lpar ss_rpar
{ $$ = NULL; }
| ss_lpar formal_comma_list ss_rpar
{ $$ = $2; }
;
pl_actuals:
ss_lpar ss_rpar
{ $$ = NULL; }
| ss_lpar exp_comma_list ss_rpar
{ $$ = $2; }
;
pushl_defstyle:
sd_id { $$ = $1; }
| s_pebble { $$ = mkstring("pebble"); }
;
pushl_def:
s_def pushl_defstyle sd_id pl_formals ss_lsect pushl_decls ss_rsect
{ $$ =
TREE4("pl_def_bundle", $2, $3, $4, $6); }
;
pushl_macro_decl:
exp12 ss_equals exp { $$ =
TREE2("", $1, $3);
}
;
pl_type:
ss_lsect value_list ss_colon value_list ss_rsect { $$ =
TREE2("pl_safeunsafe", $2, $4);
}
| ss_lsect value_list ss_rsect { $$ =
TREE1("pl_unsafe", $2); /* depreciated form */
}
| s_event { $$ =
TREE1("pl_event", LISTEND(0));
}
| s_event ss_lpar value_list_or_nil ss_rpar { $$ =
TREE1("pl_event", $3);
}
| s_fuse{ $$ =
TREE0("pl_fusetype");
}
| s_lock{ $$ =
TREE0("pl_locktype");
}
| sd_id { $$ =
TREE1("pl_tid", $1);
}
;
pushl_field_decl:
exp12_comma_list ss_colon pl_type { $$ = /* preferred form for now on */
TREE2("pl_fielddec", $1, $3);
}
| exp12_comma_list { $$ =
TREE1("pl_fielddecn", $1); /* depreciated form - no type given */
}
;
pushl_field_decl_list:
pushl_field_decl { $$ =
LISTCONS($1, LISTEND(0));
}
| pushl_field_decl ss_comma pushl_field_decl_list
{ $$ =
LISTCONS($1, $3);
}
;
pushl_macro_decl_list:
pushl_macro_decl { $$ =
LISTCONS($1, LISTEND(0));
}
| pushl_macro_decl ss_comma pushl_macro_decl_list
{ $$ =
LISTCONS($1, $3);
}
;
case_item:
s_case exp_comma_list ss_colon pushl_statement { $$ =
TREE2("pl_case_item", $2, $4);
}
| s_default ss_colon pushl_statement { $$ =
TREE1("pl_case_default", $3);
}
;
case_item_list:
case_item { $$ =
LISTCONS($1, LISTEND(0));
}
| case_item case_item_list { $$ =
LISTCONS($1, $2);
}
;
pl_assoclist:
pl_associtem { $$ =
LISTCONS($1, LISTEND(0));
}
| pl_associtem ss_comma pl_assoclist { $$ =
LISTCONS($1, $3);
}
;
pl_associtem:
sd_id ss_equals exp { $$ =
TREE2("pl_associtem", $1, $3);
}
pushl_statement:
s_sort s_set sd_id ss_equals pl_type ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_sortset_dec", $3, $5));
}
| ss_lsect pushl_statement_list ss_rsect s_fuse exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_fused", TREE1("pl_block", $2), $5));
}
| s_pragma sd_id ss_equals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_pragma", $2, $4));
}
| s_fun sd_id pl_formals ss_lsect pushl_decls ss_rsect pl_semicolon_opt { $$ =
PL_LINEPOINT(TREE3("pl_fun", $2, $3, $5));
}
| s_input pushl_field_decl_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_dv", TREE0("dv_input"), $2));
}
/* | s_lock pushl_field_decl_list ss_semicolon { $$ =
* PL_LINEPOINT(TREE1("pl_lock", $2));
* }
*/
| s_output pushl_field_decl_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_dv", TREE0("dv_output"), $2));
}
| s_inout pushl_field_decl_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_dv", TREE0("dv_inout"), $2));
}
| s_local pushl_field_decl_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_dv", TREE0("dv_local"), $2));
}
| s_facet exp ss_equals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_facet_instance", $2, $4));
}
| s_macro pushl_macro_decl_list ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_macro", $2));
}
| s_const sd_id ss_equals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_const", $2, $4));
}
| s_pebble sd_id ss_equals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_pebble", $2, $4));
}
| s_with exp pushl_statement { $$ =
PL_LINEPOINT(TREE2("pl_with", $2, $3));
}
| s_skip ss_semicolon { $$ =
PL_LINEPOINT(TREE0("pl_skip"));
}
| s_break ss_semicolon { $$ =
PL_LINEPOINT(TREE0("pl_break"));
}
| s_continue ss_semicolon { $$ =
PL_LINEPOINT(TREE0("pl_continue"));
}
| sd_id ss_colon { $$ =
PL_LINEPOINT(TREE1("pl_label", $1));
}
| s_wait exp ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_wait", $2));
}
| s_goto sd_id ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_goto", $2));
}
| s_return exp ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_return", $2));
}
| s_switch exp ss_lsect case_item_list ss_rsect { $$ =
PL_LINEPOINT(TREE2("pl_switch", $2, $4));
}
| s_disable exp_comma_list ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_disable", $2));
}
| s_meta pl_assoclist ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_meta", $2));
}
| s_live string_option exp_comma_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_live", $2, $3));
}
| s_emit exp ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_emit", $2));
}
| s_never string_option exp_comma_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_never", $2, $3));
}
| s_always string_option exp_comma_list ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_always", $2, $3));
}
| s_while ss_lpar exp ss_rpar pushl_statement { $$ =
PL_LINEPOINT(TREE2("pl_while", $3, $5));
}
| s_forever pushl_statement ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_forever", $2));
}
| s_if ss_lpar exp ss_rpar pushl_statement { $$ =
PL_LINEPOINT(TREE2("pl_if", $3, $5));
}
| s_if ss_lpar exp ss_rpar pushl_statement s_else pushl_statement { $$ =
PL_LINEPOINT(TREE3("pl_ife", $3, $5, $7));
}
| ss_lsect pushl_statement_list ss_rsect { $$ =
PL_LINEPOINT(TREE1("pl_block", $2));
}
| ss_lpsect pushl_statement_list ss_rpsect { $$ =
PL_LINEPOINT(TREE1("pl_parblock", $2));
}
| exp ss_colonequals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_assign", $1, $3));
}
| exp ss_plusequals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_assign", $1, TREE3("pl_diadic", YYLEAF("pl_plus"), $1, $3)));
}
| exp ss_minusequals exp ss_semicolon { $$ =
PL_LINEPOINT(TREE2("pl_assign", $1, TREE3("pl_diadic", YYLEAF("pl_minus"), $1, $3)));
}
| exp ss_semicolon { $$ =
PL_LINEPOINT(TREE1("pl_e_as_c", $1));
}
| s_stategraph sd_id pl_formals ss_lsect pushl_statechartlist ss_rsect ss_semicolon { $$ =
TREE3("pl_stategraph", $2, $3, $5);
}
;
pushl_statechartlist:
/* nothing */
{ $$ =
LISTEND(0);
}
| pushl_state pushl_statechartlist { $$ = LISTCONS($1, $2); }
;
pushl_statename:
sd_id { $$ = $1; }
| s_disable { $$ = mkstring("disable"); }
;
pushl_state:
s_state pushl_statename pl_formals ss_colon pushl_stateitemlist s_endstate { $$ =
TREE3("pl_state_def", $2, $3, $5);
}
| s_state pushl_statename ss_colon pushl_stateitemlist s_endstate { $$ =
TREE3("pl_state_def", $2, 0, $4);
}
;
pushl_stateitemlist:
/* nothing */
{ $$ =
LISTEND(0);
}
| pushl_stateitem pushl_stateitemlist { $$ = LISTCONS($1, $2); }
;
pushl_stateitem:
pushl_statement { $$ = /* implied body: */
TREE2("pl_state_action", mkstring("body"), PL_LINEPOINT($1));
}
| sd_id ss_colon pushl_statement { $$ =
TREE2("pl_state_action", $1, PL_LINEPOINT($3));
}
| s_exit ss_colon pushl_statement { $$ =
TREE2("pl_state_action", mkstring("exit"), PL_LINEPOINT($3));
}
| pushl_statespec ss_rarrow1 pushl_statespec ss_semicolon { $$ =
TREE3("pl_transition", $1, $3, TREE0("NONE"));
}
| pushl_statespec ss_rarrow1 pushl_statespec ss_colon pushl_statement { $$ =
TREE3("pl_transition", $1, $3, TREE1("SOME", PL_LINEPOINT($5)));
}
;
string_option:
/* nothing */ { $$ = TREE0("NONE"); }
| sd_string ss_colon { $$ = TREE1("SOME", $1); }
;
pushl_statespec:
exp { $$ =
TREE1("pl_state_exp", $1);
}
| s_exit{ $$ =
TREE0("pl_state_exit");
}
| s_exit ss_lpar sd_id ss_rpar{ $$ =
TREE1("pl_state_tagged_exit", $3);
}
;
/*
*
*/
sd_id_comma_list:
/* nothing */
{ $$ =
LISTEND(0);
}
| sd_id { $$ = LISTCONS($1, LISTEND(0)); }
| sd_id ss_comma sd_id_comma_list { $$ = LISTCONS($1, $3); }
;
exp12_comma_list:
exp12 { $$ = LISTCONS($1, LISTEND(0)); }
| exp12 ss_comma exp12_comma_list { $$ = LISTCONS($1, $3); }
;
exp_comma_list:
exp { $$ =
LISTCONS($1, LISTEND(0));
}
| exp ss_comma exp_comma_list
{ $$ =
LISTCONS($1, $3);
}
;
pl_formal:
exp ss_colon exp { $$ =
TREE2("pl_formal", $1, $3);
}
| exp { $$ =
TREE1("pl_formal_nt", $1);
}
;
formal_comma_list:
pl_formal { $$ =
LISTCONS($1, LISTEND(0));
}
| pl_formal ss_comma formal_comma_list
{ $$ =
LISTCONS($1, $3);
}
;
value:
sd_number ss_dotdot sd_number { $$ =
TREE2("pl_num_range", $1, $3);
}
| sd_number ss_minus sd_number { $$ =
TREE2("pl_num_range", $1, $3);
fprintf(stderr, " Syntax change: Please use .. instead of - for integer ranges\n");
}
| sd_id { $$ =
TREE1("pl_id", $1);
}
| ss_ellipsis { $$ =
TREE0("pl_ellipsis");
}
| sd_number { $$ =
TREE1("pl_num", $1);
}
| sd_string
{ $$ =
TREE1("pl_string", $1);
}
;
value_list_or_nil:
/* */ { $$ = LISTEND(0); }
| value_list { $$ = $1; }
;
value_list:
value
{ $$ =
LISTCONS($1, LISTEND(0));
}
| value value_list
{ $$ =
LISTCONS($1, $2);
}
;
exp:
exp1 { $$ = $1; }
;
exp1:
exp2 ss_query exp1 ss_colon exp1 { $$ =
TREE3("pl_query", $1, $3, $5);
}
| exp2 { $$ = $1; }
;
exp2:
exp3 { $$ = $1; }
| exp3 ss_rarrow2 exp3 { $$ =
TREE3("pl_diadic", YYLEAF("pl_implies"), $1, $3);
}
;
exp3:
exp4 { $$ = $1; }
| exp3 ss_rarrow2 exp4 { $$ =
TREE2("pl_implies", $1, $3);
}
;
exp4:
exp5 { $$ = $1; }
| exp4 ss_logor exp5 { $$ =
TREE3("pl_diadic", YYLEAF("pl_logor"), $1, $3);
}
| exp4 ss_disj exp5 { $$ =
TREE3("pl_diadic", YYLEAF("pl_logor"), $1, $3);
}
;
exp5:
exp6 { $$ = $1; }
| exp5 ss_logand exp6 { $$ =
TREE3("pl_diadic", YYLEAF("pl_logand"), $1, $3);
}
| exp5 ss_caret exp6 { $$ =
TREE3("pl_diadic", YYLEAF("pl_xor"), $1, $3);
}
| exp5 ss_conj exp6 { $$ =
TREE3("pl_diadic", YYLEAF("pl_logand"), $1, $3);
}
;
exp6:
exp7 { $$ = $1; }
| exp7 ss_deqd exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_deqd"), $1, $3);
}
| exp7 ss_dned exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_dned"), $1, $3);
}
| exp7 ss_dltd exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_dltd"), $1, $3);
}
| exp7 ss_dled exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_dled"), $1, $3);
}
| exp7 ss_dgtd exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_dgtd"), $1, $3);
}
| exp7 s_FQGT exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_fqgt"), $1, $3);
}
| exp7 ss_dged exp7 { $$ =
TREE3("pl_diadic", YYLEAF("pl_dged"), $1, $3);
}
;
exp7:
exp8 { $$ = $1; }
| exp9 ss_stile exp8 { $$ =
TREE3("pl_diadic", YYLEAF("pl_binor"), $1, $3);
}
;
exp8:
exp9 { $$ = $1; }
| exp8 ss_ampersand exp9 { $$ =
TREE3("pl_diadic", YYLEAF("pl_binand"), $1, $3);
}
;
exp9:
exp9 ss_plus exp10 { $$ =
TREE3("pl_diadic", YYLEAF("pl_plus"), $1, $3);
}
| exp9 ss_minus exp10 { $$ =
TREE3("pl_diadic", YYLEAF("pl_minus"), $1, $3);
}
| exp10 { $$ = $1; }
;
exp10:
exp10 ss_star exp11 { $$ =
TREE3("pl_diadic", YYLEAF("pl_multiply"), $1, $3);
}
| exp10 ss_slash exp11 { $$ =
TREE3("pl_diadic", YYLEAF("pl_divide"), $1, $3);
}
| exp10 ss_percent exp11 { $$ =
TREE3("pl_diadic", YYLEAF("pl_mod"), $1, $3);
}
| exp11 { $$ = $1; }
;
exp11:
ss_caret exp12 { $$ =
TREE1("pl_differentiate", $2);
}
| exp12 { $$ = $1; }
;
exp12:
ss_hash exp12a {
$$ = TREE1("pl_wfield", $2);
}
| exp12a { $$ = $1; }
;
exp12a:
exp12a ss_hash exp13 {
$$ = TREE2("pl_raw_field", $1, $3);
}
| exp13 { $$ = $1; }
;
exp13:
exp13a ss_lpar ss_rpar { $$ =
TREE2("pl_apply", $1, NULL);
}
| exp13a ss_lpar exp_comma_list ss_rpar { $$ =
TREE2("pl_apply", $1, $3);
}
| ss_lpar exp ss_comma exp_comma_list ss_rpar { $$ =
TREE1("pl_tuple", LISTCONS($2, $4));
}
| exp13a { $$ = $1; }
| ss_lpar exp ss_rpar { $$ = $2; }
| ss_query exp13
{ $$ =
TREE1("pl_channel_read", $2);
}
| sd_number
{ $$ =
TREE1("pl_num", $1);
}
| sd_string
{ $$ =
TREE1("pl_string", $1);
}
| ss_tilda exp13
{ $$ =
TREE1("pl_binnot", $2);
}
| ss_pling exp13
{ $$ =
TREE1("pl_lognot", $2);
}
;
exp13a:
sd_id { $$ = TREE1("pl_id", $1); }
| sd_string { $$ = TREE1("pl_string", $1); }
| exp13a ss_dot exp13a { $$ = TREE3("pl_diadic", YYLEAF("pl_cat"), $1, $3); }
| ss_dollars { $$ = TREE0("pl_dollars"); }
;
%%
#include <stdio.h>
#include <ctype.h>
extern FILE *stderr;
int yyerror (const char *s)
{
extern builder *lishlex();
extern void exit(int);
extern void givesrcPoint();
givesrcPoint();
fprintf(stderr, "Syntax error: %s: \n", s);
fprintf(stderr, "Next symbol: %s\n", atom_to_str(lishlex()));
exit(1);
return 1;
}
void yydebug_on()
{
#ifdef YYDEBUG
// extern int yydebug;
// yydebug = 0;
#endif
}
char *smllib = "plgram";
int yylex()
{
char s; int v=0;
extern void givesrcPoint();
extern builder *lishlex();
extern int lextracef;
builder *b, *a = lishlex();
if (!a) return 0;
yylval.auxval = a;
if (fnumberp(a)) return sd_number;
if (fstringp(a)) return sd_string;
b = fgetprop(a, smacro);
if (lextracef) printf("Lex %i %p %s\n", v, b, atom_to_str(a)); fflush(stdout);
if (b) return atom_to_int(fcdr(b));
s = atom_to_str(a)[0];
if (isalpha(s) || s=='_') return sd_id;
givesrcPoint();
cbgerror(cbge_fatal, "Illegal input token %c", s);
return 0;
}
/* eof */
The abstract syntax tree is defined using the following SML datatype:
(*
* $Id: plgram.sml,v 1.27 2008/07/11 08:15:04 djg11 Exp $
# CBG Badger Tuplers Project
# University of Cambridge
# Computer Laboratory
# (C) 2004 David J Greaves
#
# Mostly Written Romsey - Dec 2004.
#
# 1-Oct-05 added parblock and fuse
#
*)
open linepoint;
datatype pl_diop_t = pl_deqd | pl_dned | pl_dltd | pl_dled | pl_dged | pl_dgtd | pl_logand | pl_logor | pl_binor | pl_binand | pl_plus | pl_minus | pl_implies | pl_multiply | pl_divide | pl_mod | pl_fqgt | pl_xor | pl_cat | pl_filler_diop
;
datatype pl_type_t =
pl_safeunsafe of pl_exp_t list * pl_exp_t list
| pl_unsafe of pl_exp_t list
| pl_safe of pl_exp_t list
| pl_event of pl_exp_t list
| pl_fielddec of pl_exp_t list * pl_type_t
| pl_fielddecn of pl_exp_t list (* depreciated form *)
| pl_tid of string
| pl_fusetype
| pl_locktype
and pl_formal_t =
pl_formal of pl_exp_t * pl_exp_t
| pl_formal_nt of pl_exp_t
and pl_exp_t =
pl_query of pl_exp_t * pl_exp_t * pl_exp_t
| pl_raw_field of pl_exp_t * pl_exp_t (* comes in this way from parser *)
| pl_string of string
| pl_wtuple of pl_exp_t list (* no longer generated *)
| pl_tuple of pl_exp_t list
| pl_id of string
| pl_ellipsis
| pl_backstop
| pl_dollars
| pl_differentiate of pl_exp_t
| pl_wfield of pl_exp_t
| pl_diadic of pl_diop_t * pl_exp_t * pl_exp_t
| pl_catenate of pl_exp_t * string
| pl_num of int
| pl_num_range of int * int
| pl_lognot of pl_exp_t
| pl_apply of pl_exp_t * pl_exp_t list
| pl_par of pl_exp_t * pl_exp_t
(* The following do/does not occur in yacc parse tree *)
| pl_raw_fieldl of pl_exp_t list
| pl_filler1 (* Used only to supress the unused cases warning in my other match traps *)
;
(* Old form, compiled bytecode files: *)
datatype pl_comp_t =
pl_stringtab of string * int
| pl_bytecode of int
;
datatype xml_t =
xml_element of string * xml_att_t list * xml_t list
| xml_meta of string
| xml_int of int
| xml_chars of string
and xml_att_t = xml_att of (string * string)
;
(* A transitioner should be one of entry | body | exit *)
type pl_transitioner_t = string;
datatype dv_t = dv_output | dv_input | dv_inout | dv_local | dv_fuse | dv_lock | dv_tuple | dv_other;
datatype pl_case_item_t =
pl_case_item of pl_exp_t list * pl_cmd_t
| pl_case_default of pl_cmd_t
and pl_cmd_t =
pl_if of pl_exp_t * pl_cmd_t
| pl_while of pl_exp_t * pl_cmd_t
| pl_forever of pl_cmd_t
| pl_ife of pl_exp_t * pl_cmd_t * pl_cmd_t
| pl_switch of pl_exp_t * pl_case_item_t list
| pl_assign of pl_exp_t * pl_exp_t
| pl_pragma of string * pl_exp_t
| pl_block of pl_cmd_t list
| pl_parblock of pl_cmd_t list
| pl_with of pl_exp_t * pl_cmd_t
| pl_fused of pl_cmd_t * pl_exp_t
| pl_wait of pl_exp_t
| pl_goto of string
| pl_label of string
| pl_break
| pl_continue
| pl_emit of pl_exp_t
| pl_return of pl_exp_t
| pl_assert_sl of string * bool * pl_exp_t
| pl_never of string option * pl_exp_t list
| pl_always of string option * pl_exp_t list
| pl_live of string option * pl_exp_t list
| pl_disable of pl_exp_t list
| pl_skip
| pl_dv of dv_t * pl_type_t list
| pl_macro of (pl_exp_t * pl_exp_t) list
| pl_linepoint of linepoint_t * pl_cmd_t
| pl_pebble of string * pl_exp_t
| pl_const of string * pl_exp_t
| pl_e_as_c of pl_exp_t
| pl_sortset_dec of string * pl_type_t
| pl_meta of pl_associtem_t list
| pl_bundle of string * pl_cmd_t list
| pl_def_pebble of string * pl_formal_t list * pl_cmd_t list
| pl_def_bundle of string * string * pl_formal_t list * pl_cmd_t list
| pl_facet_instance of pl_exp_t * pl_exp_t
| pl_fun of string * pl_formal_t list * pl_cmd_t list
| pl_stategraph of string * pl_formal_t list * pl_state_t list
| pl_compiled_bundle of pl_comp_t list
| pl_xml of xml_t
| pl_filler2 (* Used only to supress the unused cases warning in my other match traps *)
and pl_associtem_t =
pl_associtem of string * pl_exp_t
and pl_state_t =
pl_state_def of string * pl_formal_t list list * pl_stateitem_t list
and pl_stateitem_t =
pl_transition of pl_statespec_t * pl_statespec_t * pl_cmd_t option
| pl_state_action of pl_transitioner_t * pl_cmd_t
and pl_statespec_t =
pl_state_exp of pl_exp_t
| pl_exit_state_exit
| pl_exit_state_tagged_exit of string
;
datatype metainfo_t =
MIA of string * string
| MIA_filler
;
(* eof *)
A Pushlogic Source program is an unordered list of declarations, bundle, pebble and function definitions. A simple program file contains just one bundle definition that contains all of the rules as well as further declarations.
Comments are defined with the BCPL-style double slash.
def bundle mybundlename()
{
// contents go here.
}
A bundle declaration uses the keyword sequence `def bundle'. The bundle content is a list of declarations and statements. The bundle name should commonly be the same as the program file name on the storage media.
The statements in a bundle are all started in parallel when the compiled object bundle is loaded. A statement may be a sequential block, thereby providing the normal imperative programming paradigm.
Each item within a bundle definitions is either a declaration, a
first-order or temporal logic assertion or an executable sequence of
imperative code. Executable sequences are composed in parallel. Each
sequence may be considered to be enclosed in an infinite while
loop that has its own thread that executes the rule as fast as
possible, but with all such threads of the bundle performing their
next assignments in synchronism. Sequential composition of
behavioural statements is introduced with the block construct, denoted
with C-like open and close braces. A further level of parallelism is
possible inside a sequential block because parallel assignment is
supported: e.g.
.
Bundles may also be declared using `def pebble', `def world' and `def plant'. The pebble declaration allows soft pebbles to be defined fully using Pushlogic. Pebbles have slightly different rules over binding of shared fields from bundles ... details to follow.
Constants may take the same forms as those define in §3.1 for object level, except that bottom is not allowed at source level.
Identifiers appear alone or as part of an heirarchic field name.
Identifiers appearing alone must be either a member of one or more field range enumerations, the last component of an heirarchic field name or the reserved identifiers `true' or `false'.
Where the last component of an heirarchic field name is shared over more than one field, or is also a constant value from a field range enumeration, the identifier cannot be used alone: it must be placed in double quotes to imply the constant value, or to refer to a field, must be disambiguated by providing further trailing portions of the heirarchic field name or using by using a `with' statement.
The alone use of identifiers is not currently working in the compiler always.
Variables are known as fields.
Field declarations define the heirarchic name of the field (its name) and then (partially) enumerate the ranges of safe values and unsafe values, delimited with colons. The safe and unsafe enumerations for must be disjoint for any one field. If the colon between the safe and unsafe values is ommitted, all listed values are unsafe.
Field values can be enclosed in quotes when they need to contain non-alphanumeric characters for any reason. An integer range is specified with a two dots. Elipsis is allowed as an unsafe value, represented with three dots.
Declarations may be introduced with the following keywords: input, output, inout, lock, local, macro and fuse. Any number of the same sort may be declared in one statement using commas to separate them.
Some examples are
input a#b#c1 : { s0, s1 : v1, v2 };
output a#b#c2 : { 0 : 1..99 };
inout e#c3 : { off : 1..9, ... };
local david : { contented : happy, sad };
Because Pushlogic is designed to operate in a dynamic, extensible environment, further values of the fields may occur at run-time, beyond those defined and checked against at compile time. Not every field name needs be declared, provided the compiler has sufficient information overall to work out the sensitive parent list to put in each object level rule.
The `input' declaration defines a field that is only read by the bundle. The `output' declaration defines a field that is only written by the bundle. The `inout' declaration defines a field that is both read and written. The writes to an inout field are frequently not explicit in the source code because they arise only during a pushback. Definition of a field as input instead of inout can lead to a `no suitable sensitive parent setting' error from the compiler.
The `local' declaration defines a field that is allocated space in the bundle's local tuple.
The `macro' declaration defines a name of a subexpression that is macro expanded before use. This might be deleted in future.
The `lock' modifier defines a field that supports atomic operations. See §5.10.15.
The `event' modifier defines a field that communicates an event. See §3.2.
The `fuse' modifier defines a field of Boolean sort that is given low priority for pushback. See §5.10.16. The range declaration for a fuse is optional, and if provided, must be `{ false : true }'.
When a modifier appears without a preceeding declaration keywork then a local declaration is made.
The `sort set' statement associates a user's idenfitier with a pair of safe and unsafe range enumerations. It can then be used in declarations, as shown in this example:
sort set mysort = { s0, s1 : v1, v2 };
output x#b, x#c : mysort;
inout x#d : mysort;
All tuples exist in a global name space, but aliases or handles for certain points are provided for ease of reference. The available handles are denoted with
| Leading Symbol | Meaning |
| dollars ($) | Local Bundle Private Namespace |
 blank |
Device/Platform Namespace |
| hash (#) | Device Namespace or with context |
| slash (/) | DoP Root |
| tup:// | URI - remote tuple access |
Hash and slash are inter-changeable as delimiters between the parts of an heirarchic field reference but have special meaning at the start of a field name. Dot may also be used, but is intended for access to components within the OO parts of the language.
A field name starting with a dollars sign is a local field name. These need not be used, since the compiler provides the special ` local' keyword that defines aliases so that local variables may be stored in the bundle's private area. In an implementation, the dollars symbol is mapped during re-hydration to a fresh tuple stored on the local execution platform whose primary key is the bundle instance identifier.
When the name starts with a hash it is interpreted with respect to the field prefix given in a textually surrounding `with' statement. If there is no surrounding `with' statement then the reference is to the namespace of the local device. This is also the default namespace when no leading character is given and the field reference starts with a tuple name.
A field name starting with a slash refers to fields provided and stored within the current DoP.
Field names may also start with a URI or a symbolic name that is converted to a URI during re-hydration. A more detailed description of heirarchic names is outside the definition of Pushlogic and are defined in the Tuplecore document and web pages.
The `pebble' alias statment establishes a pointer to part of the namespace. It is frequently used to provide a Pushlogic bundle with access to pebbles instantiated on the same device (platform), hence its name, but it can also be used for access to fields shared by other bundles.
Here we present a simple example using hardwired IP address, but actual device addresses should not normally appear in the source code: they should be supplied during re-hydration:
def bundle simplelink()
{
pebble my_keyboard = Pebbles#Front_panel#Keyboard;
pebble your_devices = tup://128.232.1.10/Pebbles#Devices;
// field declarations omitted
your_devices#front_panel#on_led := my_keyboard#on_switch;
}
Pebble aliases can be defined inside a bundle statement (as shown) or outside.
The `pragma' statment enables control flags to be passed to the compiler. These may occur inside a bundle declaration or at the top level of a file. See the compiler manual for details of the supported pragmas.
The operators available at source level include all those defined in for object level in §4.3. Each is denoted with its usual symbol or digraph.
In addition, the differentiate operator is provided, denoted with uparrow ( 
exp).
The currently available forms are summarised in Figure 5.1.
It is our goal to support as many features found in common OO imperative HLLs as possible, while still producing output that can be represented as Pushlogic object rules and checked automatically at load time.
Function calls are expanded fully at compile time and so must be have statically bounded recursion.
The `emit' statement delivers a Pushlogic event. This may be mapped to a non-Pushlogic GENA event or device RPC during rehydration (§5.11.1).
if (<ee>) emit <event-name>; if (<ee>) emit <event-name>(args, ...);
The `emit' statement is shown in the context of an `if' statement that is guarded by an event expression. Such a guard must normally exist within the surrounding program flow control in some form or another.
If the guard is a level expression, this would allow cause a nominal, continuous stream of back-to-back events to be emitted and would tend to violate idempotency.
The guarding context may be a level expression if the event being emitted is entirely local and the nominal stream of events is local to the current bundle and is integrated back to being a level expression in all places where it is used.
In the future, it is envisaged that closer integration with UPnP, SOAP and other device control languages will be implemented, and hence the emit statement will be implied by constructs such as
if (<ee>)
house.livingroom.curtains.setto(halfway);
This need arises since many devices have an event-driven API and integrate the received event stream to set their internal state; these are conventional models of commanding over an asynchronous packet network.
The pebble statement is used to hard-code the address of a network resource, such as the IP address and port number of a remote pebble. This statement should not normally be used and should not occur in portable code. Binding is normally performed at rehydration time, mapping symbolic constants in the source code to active network addresses.
def bundle displayecho()
{
pebble PushClock = "tup://169.254.25.32:1200";
input PushClock#Pebbles#ClockDisplay#Leds#hour : {0..23};
input PushClock#Pebbles#ClockDisplay#Leds#minute : {0..59};
pebble DisplayPanel = "tup://169.254.25.192:1202";
output DisplayPanel#Pebbles#Display#value : { "No message yet" : ... };
// Use the string cat operator, dot, to make the output message.
value := "Time now:" . hour . " " . minute;
}
Assignments are denoted with the colon-equals assignment operator.
Parallel assignment is supported where the same number of
comma-separated expressions appear on both sides of the assignment :
e.g.
.
All executable rules are placed in parallel by default at the top-level but sequential composition occurs inside nested blocks, unless explicitly written in this parallel form.
The constraints on the object-level assignments between level and event variables and expressions, given in §4.6.2, is reflected at the source level, but with one relaxation, described in §5.10.1.
The object-level constraints allow the following four basic source forms, or anything tantamount to them:
if (le) lv := le; if (le) ev := ee; if (ee) lv := le; if (le) lv := ee;
Rather than assigning to an event variable, emitting an event is possible, described in §5.10.1.
The third and fourth forms are known as integrations.
Statements separated by a semicolon inside a `bundle', `def mod' or top-level `with' with statment are still considered top-level and composed in parallel. All other statements separated by a semicolon are composed in series, corresponding to normal imperative programming.
An example:
def bundle s()
{ // Bundle braces do not force seq
...
a := b; // Three statements in parallel (two assigns and an if).
c := d;
if (e)
{
f := h; // A seqeuence of two statements.
g := f+j; // Assign to f above has immediate effect on this rhs.
}
}
The `with' statement sets up a textually-scoped alias for part of tuple space. Field references that start with an hash sign inside the statement are refered to this alias. An example:
with (/devices#book)
{
x1 := /devices#book#page#number;
x2 := #page#number;
// x1 and x2 have actually been assigned the same.
}
The `with' statement does not cause sequential composition of its contents.
The `if/else' statement, as found in the C language, is supported.
A form of `switch' statement, is supported. Multiple tags per statement block are allowed using comma separation. Unlike the C language, flow does not fall from one branch into the next and so there is no associated binding for the `break' statement.
A tag called `default' may be used to catch any, otherwise unmatched conditions.
The stategraph defines a finite state machine, where each state has a state name. A top-level stategraph is always active, meaning it is in exactly one state. On the other hand, a stategraph that is instanced as a child stategraph within a state in another stategraph is inactive (not in any state) unless its parent is in that instantiating state. A state may instantiate any number of child stategraphs but recursion is not allowed.
The stategraph general form is:
stategraph graph_name()
{
state statename0 (subgraph_name, subgraph_entry_state), ... :
entry: statement;
exit: statement;
body: statement;
statement;
... // implied 'body:' statements
statement;
c1 -> statename1: statement;
c2 -> statename2: statement;
c3 -> exit(good);
...
exit(good) -> statename3: statement;
exit(bad) -> statename4: statement;
...
endstate
state statename2:
...
...
endstate
state disable: // A special state that can be
// forced remotely
...
}
A state may contain tagged tatements, each of which may be a basic block if required. They are distinguished using three tag words. The `entry' statement is run on entry to the state and the `exit' statement is run on exit. The `body' statement is run while in the state. A `body' statement must contain idempotent code, so that there is no concept of the number of times it is run while in the state. Statements with no tag are treated as body tagged statements. Multiple occurrences of statements with the same tag are allowed and these are evaluated as though executed in the textual order they occur or else in parallel (current implementation is serial but this will be change to parallel, so watch out!).
A state contains transition definitions that define the successor states. Each transition consists of a boolean guard expression, the name of one of the states in the current stategraph and an optional statement to be executed when taking the transition. In situations where multiple guard expressions currently hold, the first holding transition is taken.
The guard expressions range over the inputs to the stategraph, which are the variables and events in the current textual scope, and the exit labels of child stategraphs.
When a child stategraph becomes active, it will start in the starting state name is given as an argument to the instantiation, or the first state of no starting name is given.
A child stategraph becomes inactive when its parent transitions, even if the transition is to the current state, in which case the child stategraph becomes inactive and active again and so transitions to the appropriate entry state.
A child stategraph can cause its parent to transition when the child transitions to an exit state. There may be any number, including zero, of exit states in a child stategraph but never any in a top-level stategraph. The parent must define one or more transitions to be taken for all possible exit transitions of its children. An exit state is either called 'exit' or 'exit(id)' where 'id' is an exit tag identifier. Exit tags used in the children must all be matched by transitions in the parent, or else the parent must transition itself under the remaining exit conditions of the child or else the parent must provide an untagged exit that is used by default.
A stategraph may be wholly enclosed inside any conditional statement, such as an `if' or `case' statement, in which case it is as though all of its internal activity is guarded by that condition: the condition is simply folded inside every construct to the point where a conditional is allowed. The stategraph does not reset to its starting state when this guard does not hold.
A stategraph with a state called disable may be disabled from elsewhere in the same bundle using the `disable' statement. Please see §5.10.10.
The stategraph general form is sufficient to encompass the SysML state machines.
The `disable' statement is used for a remote disable of a stategraph.
Syntax:
if (g) disable stategraph_name1, stategraph_name2, ...;
The disable statement must be conditional, otherwise the stategraph
would never leave its disable state, and the disable guard, 
may either
be an event or level expression. When the disable guard is a level expression
it takes precedence over any transitions in the stategraph that lead from
the disable state.
if (g) disable stategraph_name1, stategraph_name2, ...;
The `while/continue/break' statement, as found in the C language, is supported.
The `for/continue/break' statement, as found in the C language, is supported.
The `do/while/continue/break' statement, as found in the C language, is not yet implemented.
The `forever' statement is an alias for `while(1)'.
A procedure call statement has no keyword. A call consists of a function name followed by its arguments in parenthesis. Procedure calls are expanded at compile time and hence must have a compile-time determined upper-bound on recursion depth.
An example:
def fun add(a, b, c)
{
if (a=red) return b;
return c+d;
}
while(1)
{
...
wait expr;
...
}
The `wait' statement cause the current `thread' to wait until a condition holds. There are no threads in Pushlogic object code and so the wait statement is implemented by splitting the source code into separate basic blocks that are guarded by values of an automatically-defined enumeration that chains control from one block to the next. The enumeration variable acts rather like a program counter. At runtime it is stored in the field `$local#pcnnn' where nnn is an integer that is unique to a bundle. To avoid inter-bundle name-space clashes, all fields in starting with `$local' are renumbered to be disjoint at bundle load time. The same mechanism is used to create a hidden variable to store the old value of a field by the differentiation operator denoted with the uparrow ().
SOME REPETITION HERE!
The wait statement blocks the current thread until the condition holds. If the thread loops around and enters the same wait statement while the condition still holds, the thread is not blocked.
Where more than one wait statement exists for a thread, a program counter variable is created and stored as a field in the bundle's local tuple.
The lock statement declares a field that supports atomic test-and-set operations.
A field of sort lock has as its safe value the empty string.
Any bundle may store a value in a lock field, but only if it is currently null. If it is not null, the write will fail and a pushback occurs. A bundle typically stores its own private identifier (accessible from the metainfo tuple §6.1).
A bundle is responsible for clearing the lock back to the empty string when it has finished with the guarded resource.
{
input X#x : { S: US };
inout Y#y : { S: US };
y : = x;
}
The problem is that if 
makes a unilateral change from US to S, which
it is free to do, since it is an `inout', then no push back is possible
because 
is an `input' that cannot be changed from inside the bundle.
The solution is to enclose the rule inside a fuse. This fuse is able to
`blow' should make a push back.
input X#x : { S: US };
inout Y#y : { S: US };
fuse F1;
{ y : = x; } fuse F1;
forever { wait F1; sleep_secs(5); F1 := false; }
The fuse declaration defines a boolean variable with both values safe and to be set false on bundle load. The fuse statement is just syntactic sugar, because the line ` y : = x; fuse F1;' is rewritten during initial expansion as `if (!f1) y : = x;'. During pushback path creation, the fuse is chosen as the last option and only marked for push back update if there is no other pushback path available. Only the inner-most fuse of any nested fuse blocks acts on the enclosed code.
The reset behaviour is enclosed inside a forever statement, equivalent
to `while (1)' and not needed since all push logic sequential sections
are enclosed inside an implied forever. It resets the fuse five seconds
after it has blown. If refuses to accept the current value
at this time, the fuse blows again. Other code can be sensitive to
this fuse.
Currently RPC is not used and all comunication between platforms is implemented via the shared-variable illusion implemented by the tuplecore `ETC' protocol. In the future, Remote procedure call (RPC) may be used between Pushlogic bundles, or between a Pushlogic bundle and a non-pushlogic entity.
Pushlogic may make calls directly over the network using XML RPC (and in the future SOAP RPC). Details to be added...
Pushlogic can also send and receive GENA events by setting up simple mappings between Pushlogic events and GENA events. Details to be added...
Native remote procedure call is provided for communication between Pushlogic bundles on the same or different execution platforms. implemented by expansion to other statements. Owing to the dynamic storage restiction limitations of SPL1, a bundle must be re-hydrated for each concurrent service operation. Blocking RPC is currently being developed - the blocking aspect is implemented by expansion to the `wait' statement.
Non-blocking RPC does not return a result and is denoted with `device!(...)' where the ellipsis is replaced with a list of assignments to mutable fields of that device. This is translated to a conjunction of assertions that the appropriate tag fields of the indexed device have the values being passed. Blocking RPC is implemented by the compiler as a combination of non-blocking RPC and a wait statement.
Details to be added here ...
Some basic syntactic sugar is implemented to enable objects to be defined and instantiated. All instantiations are performed at compile time using abstract interpretation and so must be statically determinable.
This part of the compiler is currently a bit broken, but contains nothing novel.
Assertions may be included in the Pushlogic source code and checked by the system model checker as well as at compile time or at load time, as appropriate. Each assertion can have a textual name.
A `live' assertion asserts that a condition must reoccur infinitely often. A `never' assertion asserts that a condition must never occur. An `always' assertion asserts that a (level) condition must always holds and is equivalent to a never statement with negated condition. In these assertions, any number of conditions may be listed, separated by commas, and these have the same meaning as if provided in a separate statements. Live statements may occur inside if/then/else and other control flow statements, in which case each condition is guarded by (conjuncted with) the enclosing conditional statement guards.
In the future, these simple assertions will be augmented with richer assertions that span the ground between liveness and safety: i.e. until assertions and assertions that specify quantitative maximum and minimum valuations on resource use.
always [ string : ] <exp>, <exp> ...;
never [ string : ] <exp>, <exp> ...;
live [ string : ] <exp>, <exp> ...;
The string is the rule name that is carried forward for output by logging or monitoring code.
We illustrate liveness checking using the following bundle that causes a variable called locked to be false for 5 seconds after a variable called button holds.
def bundle ButtonLock()
{
input v#keys#button : { false:true};
output v#locks#unlocked : { false:true };
forever {
wait (button);
unlocked := true;
sleep_secs(5);
unlocked := false;
wait (!button);
}
local locked := !unlocked;
live "Door Unlockable Assertion" unlocked, locked;
}
It makes a call to the following timer library function, that blocks the thread for a period, using the timer pebble provided on all execution platforms. As explained, there is no notion of thread in the final bytecode because all function calls are inlined during compilation and all thread constructs are converted to executable rule form. The live statement is an assertion that the locked variable should never become stuck at one value permanenty.
fun sleep_secs(t)
{
local until : { 0..59 };
with (__local_timer)
{ until := (#time_now#second + t);
wait(#time_now#second FQGT until);
}
}
The timer code places the unblocking time in the local variable until and then blocks. The FQGT operator is builtin and performs a greater-than comparison that behaves sensibly as the arguments overflow in their field provided their initial difference is less than half the range. In the future, we would like to use a wider field than seconds (0 to 59) so that we can sleep, say, for many thousand milliseconds. However, larger fields consume more BDD primary inputs and BDD nodes, which are currently at a premium. We shall also consider automatic switching to a lifted form for modelling the sleep call, where it is held as a single wait statment on a fresh variable. This is simpler to model, provided there are few of these constructs, but complexity will eventually mount up in meta-constraints over the fresh variables that model the possible firing orders.
Here is a bundle that is incompatible with the ButtonLock: both cannot be loaded into the same DoP. To explain this, first we must mention that we have not fully implemented the re-hydration stage yet, and so hardcoded identifiers, such as the IP address of the other bundle's platform are currently hardcoded in the source files. The button variable was originally free to change at any time but becomes constrained by the second bundle to only change while the unlocked variable holds. The system cannot be unlocked without the button being pressed, and hence the live assertion in the Button listing fails. This will in future be spotted by the DoP manager, but currently can only be spotted by the compiler checking against pre-compiled bundles that are to hand.
def bundle B2()
{
pebble r = tup://128.232.1.45/v;
input d#q : bool;
r#keys#button := r#locks#unlocked && d#q;
}
It is helpful to briefly present the internal operation of the compiler. The internal flow of the compiler is shown in Figure 5.2.
The input is parsed and converted to imperative intermediate code using conventional compiler techniques. Function calls are expanded in line. For each sequence in the source code a section of I-code is generated. I-code consists of labels, gotos, waits, assignments and conditional branches. For each section, a run-time program counter is defined. At the object code level, these program counters act just like other local variables, and their values range over the labels in that section. There is no run-time spawning or joining of threads (although the illusion of this can be provided from a static set of threads using pre-processing techniques). Temporal logic assertions in the source code are split off and held separately. Liveness assertions may be guarded by nested if statements and by the current value of the program counter.
Each I-code instruction is stored in an array, indexed by compile-time program counter, and each has one of the following forms:
(* Intermediate, imperative assembler code form *) and icode_t = I_assign of bc_t * bc_t | I_resultis of bc_t | I_goto of int | I_wait of bc_t | I_if of bc_t * int | I_eof | I_skip | I_safetylive of bool * bc_t (* safe is true *)
Runtime program counters range only over the entry point to a thread and the points immediately following an I_wait.
The I-code is embedded in a BDD package by generating binary encodings of every variable (field), constant and operator. This then enables an equivalence checker to be used to compare any pair of expressions or check that a predicate is a tautology.
An entry point is defined as any entry point to a section of I-code or the location immediately after any wait instruction. Parallel symbolic evaluation is then conducted, until closure, or failure if more than 100 iterations is needed. This consists of starting in a null environment and evaluating from each entry point to collect symbolically the assigns to every variable, including program counters, up until a wait statement or the thread loops back to its initial entry point. Function calls are expanded in line.
While more than one assign is made to a variable, by different
threads, such as
, the assignments are combined in
pairs using the following rule
Sequential composition of statements is implemented by forming a conjunction of their translations but where any assignment is implemented as as symbolic substitution before translating a next statement.
![\begin{eqnarray*}[\![v=e; C_2 ]\!]& \rightarrow & [\![v=e ]\!]\wedge [\![C_2[e/v...
...[C_1; C_2 ]\!]& \rightarrow & [\![C_1 ]\!]\wedge [\![C_2 ]\!]\\
\end{eqnarray*}](img35.png)
The if/then/else construct is converted to an object form conditional expression
![\begin{displaymath}[\![{\tt if } c {\tt then } T {\tt else F} ]\!]\rightarrow
[\![c ]\!] ? [\![T ]\!] : [\![F ]\!]
\end{displaymath}](img36.png){kind=small}
After the first elaboration from all entry points, the process is
repeated using the environment created by the first. Code guarded by
differentiators will not have any consequences on the second or subsequent
elaborations. After each elaboration, the equivalence checker is
used to detect any changes in any symbolic value, and if there are,
then another iteration is commenced. Before each new iteration,
occurrences of 
in the expression for a variable in the
environment are replaced with the symbolic value for that variable
calculated on the iteration before. This exactly models the behaviour
of the runtime interpreter, which holds (or gates) all
assignments until every subexpression has been recomputed, and then
performs a commit.
After a closed set of symbolic assignments has been computed, push back paths are created through the right-hand-side expressions from any field whose mode is 'inout'. For each safe value of an inout field, a path is traced backwards through the expression tree that will cause generation of that value. These paths extend back though local variables used as intermediate values in any computation. For all safe values of all bearing inouts, the same path must work for each local variable. This constraint can cause some novel error messages. The paths are stored in the push back indication section of each rule.
Sub-expressions are generated by spotting common subexpressions using a hashing technique. Where a pair of rules use a common subexpression, this sharing is noted by a re-writing phase before code generation.
The model checker constructs a next state relation from the executable rules. For the purposes of the relation, a hidden input variable is created for every possible pushback, which is every safe value of every inout field. This is called a pushback input. Additional clauses are added to the next state relation to represent that at most one of the pushback inputs of each inout may hold at any one time, and that when it holds, the variables altered by that pushback have the constant values determined during pushback calculation.
The dot net version can be canned to ROM by compiling it with the ilasm assembler from the mono project and then using the monos utility program on the resulting bytecode.
In the future, the declarative byte code can also be converted to C to be run as native ROM code instead of being interpreted on the execution platform (thereby saving expensive RAM on embedded devices).
The pushlogic compiler contains a symbolic model checker that uses a BDD package. This is the same BDD package as used by the compiler for equivalence checking when it is searching for idempotent closure (§5.14.2).
The model checker in the compiler can operate on more than one bundle at once, checking inter-bundle interactions. Since the compiler can accept, on its command line, at most one source file and any number of object files, there are three ways the model checker might get invoked:
The third way enables the compiler to serve as a checker over a set of rehydrated bundles. Hence it can serve as the domain checker.
Scalability is a big problem with BDD-based model checking. A fair bit of time is used up finding variable orderings that lead to a compact BDD. The compiler writes out the order it finally selected to a hidden file, .bdd.xml, and reads it in again, if present in the current directory. Since the filename is currently fixed, it is important to do widely differing runs in different directories.
Current research is developing an incremental model checker so that scalability restrictions are greatly reduced.
The compiler generates a small amount of meta information and stores this in a dedicated tuple in the local space.
Before execution and insertion into a DoP, a bundle is re-hydrated using operations akin to macro-language rewrites ...
