next up previous index
Next: Joining Automata Synthesis Up: SPL Orangepath H2 Language Previous: SPL Orangepath H2 Language   Index

Subsections

H2 Syntax

The H2 language possesses various subsets and the intention is that these may be freely mixed, at a fine level, to describe a design. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts.


Concrete syntax tree

The H2 HPR concrete syntax tree is following yacc file:

/*
 *  $Id: h2gram.yy,v 1.15 2008/11/05 12:13:34 djg11 Exp $
 *
 * Orangepath HPRLS H2 Grammar using Bigtop.  
 * (C) 2003 DJ Greaves. All rights reserved.
 * 
 */



%{
#include "cbglish.h"

//define CBG_YYDEBUG
#ifdef CBG_YYDEBUG
#define YYDEBUG 1
#endif

#define OUI_LINEPOINT(X) add_linepoint("Oui_linepoint", X)
#define OBEV_LINEPOINT(X) add_linepoint("Obev_linepoint", X)

int yyerror (const char *s);
 

%}

%union {
	builder *auxval;
       }

%type <auxval> Oh2_formals 
%type <auxval> orange_statename orange_statechartlist orange_state orange_stateitemlist orange_stateitem orange_statespec
%type <auxval> orange_decls prog module h2_imp h2_imp_list  orange_unit_item_list
%type <auxval> qexp exp exp1 exp2 exp3 exp4 exp5 exp6 exp7 exp65 exp8 exp9 exp10 exp11 exp12 exp13 exp13a orange_unit_mode orange_unit orange_unit_item orange_node_qualifier_list orange_node_qualifier onq_s_range qexp_comma_list exp_comma_list pslexp_comma_list sd_id_comma_list orange_unit_instance orange_unit_instance_comma_list orange_instance_qualified orange_instance_qualified_list built_in_type h2_mitre_option formal_list formal tnumber_list

%type <auxval> pslexp pslc pslexp1 psl_oe orange_type

%%


prog:
  orange_decls
	{
	builder *r = $1;
	results = LISTCONS(r, results);
	$$ = freverse(results);
	}
;

orange_decls	:	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| module orange_decls 
	{ $$ =
	LISTCONS($1, $2);
	}
;


/* These facet names should be lifted: we dont wish to just have this finite number of hardcoded aspects to a design. */
orange_unit_mode:
  s_interface  { $$ = TREE0("Ointerface"); }
| s_protocol   { $$ = TREE0("Oprotocol"); }
| s_section    { $$ = TREE0("Osection"); }
| s_action   { $$ = TREE0("Oaction"); }
| s_entity   { $$ = TREE0("Oentity"); }
| s_unit sd_id      { $$ = 
	TREE1("Ounitmode", $2); 
	}
;


orange_unit_instance:
  sd_id	{ $$ =
	TREE2("Oui", $1, NULL);
	}

| sd_id ss_lpar exp_comma_list ss_rpar	{ $$ =
	TREE2("Oui", $1, $3);
	}


;


orange_unit:
  s_typedef sd_id ss_equals orange_type ss_semicolon { $$ = TREE2("Ounit_typedef", $2, $4); }


| orange_unit_mode sd_id ss_lpar formal_list ss_rpar ss_lsect orange_unit_item_list ss_rsect
 	{ $$ =
	TREE4("Ounit_presence", $1, $2, $4, $7);
	}
;

orange_node_qualifier:
  s_out { $$ = 
	TREE0("Onq_out"); 
	}

| s_in {  $$ = 
	TREE0("Onq_in"); 
	}

| s_inout { $$ =  
	TREE0("Onq_inout"); 
	}

| ss_pling { $$ = 
	TREE0("Onq_pling"); 
	}

| sd_id { $$ = 
	TREE1("Onq_user", $1); 
	}

| s_forward { $$ = 	TREE0("Onq_forward"); 	}

| s_signed { $$ = 	TREE0("Onq_signed"); 	}

| s_unsigned  { $$ = 	TREE0("Onq_unsigned"); 	}
| s_initiator { $$ = 	TREE0("Onq_initiator");  }
| s_target    { $$ = 	TREE0("Onq_target"); 	}

| s_event { $$ = 
	TREE0("Onq_event"); 
	}

| s_mutex { $$ = 
	TREE0("Onq_mutex"); 
	}

| s_integer { $$ = TREE0("Onq_integer"); 	}  // hmmm, cf Ot_int

| s_channel { $$ = 	TREE0("Onq_channel"); 	}  // hmm : a channel type constructor

| s_parameter { $$ = 
	TREE0("Onq_parameter"); 
	}

| s_reverse { $$ = 
	TREE0("Onq_reverse"); 
	}

| built_in_type { $$ = 
	TREE1("Onq_bit", $1); 
	}

| onq_s_range { $$ = $1; }

/*  orange_unit_mode sd_id  { $$ = 
 	TREE2("Onq_inherit", $1, $2);
	} */
;


built_in_type:
  s_bool {     $$ = TREE0("Ot_bool");     }
| s_natural {     $$ = TREE0("Ot_natural");     }
;

orange_type:
  built_in_type { $$ = $1; }
| s_enum ss_lsect sd_id_comma_list ss_rsect  { $$ = TREE1("Ot_enum", $3); }

;


/*
 *
 */
orange_instance_qualified:
  ss_pling sd_id { $$ = 
	TREE2("Oiq_pling", $2, LISTEND(0)); 
	}

| sd_id { $$ = 
	TREE2("Oiq_id", $1, LISTEND(0)); 
	}
;


onq_s_range:
	ss_lbra  exp ss_colon exp ss_rbra 
	{ $$ = 
	TREE2("Onq_square_range", $2, $4);
	}
|	ss_lbra exp ss_dotdot exp ss_rbra 
	{ $$ = 
	TREE2("Onq_dot_range", $2, $4);
	}
|	ss_lbra  exp ss_rbra 
	{ $$ = 
	TREE1("Onq_dimension", $2);
	}

|	ss_lbra ss_rbra 
	{ $$ = 
	TREE0("Onq_undefrange");
	}
;

Oh2_formals:
  ss_lpar formal_list ss_rpar { $$ = $2; }
;

optional_semicolon: /* nothing */ | ss_semicolon
;

h2_mitre_option:
	ss_semicolon /* nothing */ { $$ =
	LISTEND(0);
	}

| s_mitre h2_imp_list optional_semicolon { $$ = 
	$2;
	}
;



orange_unit_item:
  s_stategraph sd_id exp_comma_list ss_lsect orange_statechartlist ss_rsect ss_semicolon  { $$ =
	TREE3("Oui_stategraph",  $2, $3, $5);
	}

	
|  s_node orange_node_qualifier_list  ss_colon orange_instance_qualified_list  ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_node_decl", $2, $4));
	}

|  s_parameter orange_node_qualifier_list  ss_colon orange_instance_qualified_list  ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_node_decl", LISTCONS(TREE0("Onq_parameter"), $2), $4));
	}

|  s_event orange_node_qualifier_list  ss_colon orange_instance_qualified_list  ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_node_decl", LISTCONS(TREE0("Onq_event"), $2), $4));
	}

|  s_channel orange_node_qualifier_list  ss_colon orange_instance_qualified_list  ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_node_decl", LISTCONS(TREE0("Onq_channel"), $2), $4));
	}

|  orange_unit_mode sd_id ss_colon orange_unit_instance_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE3("Oui_instance", $1, $2, $4));
	}

|  ss_lsect h2_imp_list ss_rsect  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_bev", TREE0("NONE"), $2));
	}


|  s_process ss_lpar exp ss_rpar ss_lsect h2_imp_list ss_rsect  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_bev", TREE1("SOME", $3), $6));
	}

| orange_unit_mode sd_id ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE3("Oui_instance", $1, $2, NULL)); /* null means exactly one anonymous instance */
	}

| s_connect sd_id ss_colon exp_comma_list h2_mitre_option  { $$ = 
	OUI_LINEPOINT(TREE3("Oui_connect", TREE1("SOME", $2), $4, $5));
	}
| s_connect sd_string ss_colon exp_comma_list h2_mitre_option { $$ = 
	OUI_LINEPOINT(TREE3("Oui_connect", TREE1("SOME", $2), $4, $5));
	}


| s_const sd_id ss_equals exp ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_const", $2, $4));
	}

| s_always pslexp_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_temporal", TREE0("Oalways"), $2));
	}
| s_idle pslexp_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_temporal", TREE0("Oidle"), $2));
	}
| s_initial pslexp_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_temporal", TREE0("Oinitial"), $2));
	}
| s_never pslexp_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_temporal", TREE0("Onever"), $2));
	}

| s_fair pslexp_comma_list ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_temporal", TREE0("Ofair"), $2));
	}

| exp ss_colonequals exp ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_colonassign", $1, $3));
	}

| s_fundef sd_id Oh2_formals ss_lsect  h2_imp_list ss_rsect  { $$ = 
	OUI_LINEPOINT(TREE3("Oui_fundef", $2, $3, $5));
	}



| s_statevar sd_id orange_type ss_semicolon  { $$ = 
	OUI_LINEPOINT(TREE2("Oui_statevar_decl", $2, $3));
	}


|  s_neutral ss_colon { $$ = 
	OUI_LINEPOINT(TREE0("Oui_neutral"));
	}

|  s_forward ss_colon { $$ = 
	OUI_LINEPOINT(TREE0("Oui_forward"));
	}

|  s_reverse ss_colon { $$ = 
	OUI_LINEPOINT(TREE0("Oui_reverse"));
	}
;



module:
   orange_unit { $$ = $1; }

 
   /* This one will be depreciated in future */
|  s_simplebev ss_lpar ss_rpar  ss_lsect  h2_imp_list ss_rsect
	{ $$ =
	TREE2("Osimplebev", nil, $5);
	}

;






orange_statechartlist:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| orange_state orange_statechartlist { $$ = LISTCONS($1, $2); }
;

orange_statename:
   sd_id { $$ = $1; }
|  s_abort { $$ = mkstring("disable"); }
;


orange_state: 
  s_state orange_statename  ss_lpar exp_comma_list  ss_rpar ss_colon orange_stateitemlist s_endstate { $$ =
	TREE3("Oh2_state_def",  $2, $4, $7);
	}
| s_state orange_statename ss_colon orange_stateitemlist s_endstate { $$ =
	TREE3("Oh2_state_def",  $2, 0, $4);
	}
;

orange_stateitemlist:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| orange_stateitem orange_stateitemlist { $$ = LISTCONS($1, $2); }
;


orange_stateitem:
  h2_imp { $$ = /* implied body: */
	TREE2("Oh2_state_action", mkstring("body"), OBEV_LINEPOINT($1));
	}
| sd_id  ss_colon h2_imp { $$ =
	TREE2("Oh2_state_action", $1, OBEV_LINEPOINT($3));
	}

| s_exit  ss_colon h2_imp { $$ =
	TREE2("Oh2_state_action", mkstring("exit"), OBEV_LINEPOINT($3));
	}

| orange_statespec ss_rarrow1 orange_statespec ss_semicolon { $$ =
	TREE3("Oh2_transition", $1, $3, TREE0("NONE"));
	}

| orange_statespec ss_rarrow1 orange_statespec ss_colon h2_imp { $$ =
	TREE3("Oh2_transition", $1, $3, TREE1("SOME", OBEV_LINEPOINT($5)));
	}
;


orange_statespec:
  exp { $$ =
	TREE1("Oh2_state_exp", $1);
	}
| s_exit{ $$ =
	TREE0("Oh2_state_exit");
	}
| s_exit ss_lpar sd_id ss_rpar{ $$ =
	TREE1("Oh2_state_tagged_exit", $3);
	}

;




orange_unit_item_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| orange_unit_item orange_unit_item_list
	{ $$ =
	LISTCONS($1, $2);
	}
;

sd_id_comma_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| sd_id { $$ = LISTCONS($1, LISTEND(0)); }

| sd_id ss_comma sd_id_comma_list { $$ = LISTCONS($1, $3); }
;


orange_unit_instance_comma_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| orange_unit_instance { $$ = LISTCONS($1, LISTEND(0)); }

| orange_unit_instance ss_comma orange_unit_instance_comma_list { $$ = LISTCONS($1, $3); }
;


psl_oe:
  sd_id { $$ =
	TREE1("Oid", $1);
	}

| sd_id ss_dot psl_oe	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ocatenate"), TREE1("Oid", $1), $3); 
	}

| ss_lpar exp ss_rpar { $$ = $2; }

| sd_number
    { $$ =
	TREE1("Onum", $1);
	}

| sd_string
    { $$ =
	TREE1("Ostring", $1);
	}

| ss_tilda psl_oe
	{ $$ =
	TREE1("Obinnot", $2);
	}

| ss_pling psl_oe
	{ $$ =
	TREE1("Olognot", $2);
	}
;


pslc:
  psl_oe		   { $$ = TREE1("Pslc_o2", $1); } 
| ss_rarrow1 exp9 	   { $$ = TREE2("Pslc1", $2, TREE0("goto")); }
| ss_star exp9  	   { $$ = TREE2("Pslc1", $2, TREE0("star")); }
| ss_equals exp9  	   { $$ = TREE2("Pslc1", $2, TREE0("equals")); }
| ss_plus  		   { $$ = TREE0("Pslc_plus"); }
| ss_rarrow1   	   	   { $$ = TREE0("Pslc_goto"); }
;

pslexp1:
  psl_oe			{ $$ = TREE1("Psl_leaf", $1); }
| ss_lsect pslexp1 ss_rsect 	{ $$ = $2; }

| pslexp1 ss_lbra pslc ss_rbra 	{ $$ = TREE2("Psl_rep1", $1, $3); }
| pslexp1 ss_lbra pslc ss_colon pslc ss_rbra{ $$ = TREE3("Psl_rep2", $1, $3, $5); }


| pslexp1 ss_semicolon pslexp1 	{ $$ = TREE3("Psl_diadic", TREE0("catenate"), $1, $3); }
| pslexp1 ss_colon pslexp1 	{ $$ = TREE3("Psl_diadic", TREE0("fusion"), $1, $3); }
| pslexp1 ss_logand pslexp1 	{ $$ = TREE3("Psl_diadic", TREE0("matchconj"), $1, $3); }
| pslexp1 ss_ampersand pslexp1 	{ $$ = TREE3("Psl_diadic", TREE0("conjunction"), $1, $3); }
| pslexp1 ss_stile pslexp1	{ $$ = TREE3("Psl_diadic", TREE0("alternate"), $1, $3); }
| pslexp1 s_within pslexp1 	{ $$ = TREE3("Psl_diadic", TREE0("within"), $1, $3); }
;


//
// The full PSL language is handled by pslexp1 but pslexp supports some of the
// psl operators without the need for an outer pair of braces.
//
pslexp:
  exp				{ $$ = TREE1("Psl_leaf", $1); }
| ss_lsect pslexp1 ss_rsect 	{ $$ = $2; }
| pslexp s_within pslexp 	{ $$ = TREE3("Psl_diadic", TREE0("within"), $1, $3); }
| s_rose exp11	  		{ $$ = TREE1("Psl_leaf", TREE2("Opsl_builtin", mkstring("rose"), $2)); }
| s_fell exp11			{ $$ = TREE1("Psl_leaf", TREE2("Opsl_builtin", mkstring("fell"), $2)); }
| s_stable exp11		{ $$ = TREE1("Psl_leaf", TREE2("Opsl_builtin", mkstring("stable"), $2)); }
| s_next exp11			{ $$ = TREE1("Psl_leaf", TREE2("Opsl_builtin", mkstring("next"), $2)); }
| s_prev exp11			{ $$ = TREE1("Psl_leaf", TREE2("Opsl_builtin", mkstring("prev"), $2)); }
;


pslexp_comma_list:
	/* nothing */
	{ $$ =	LISTEND(0); }
| pslexp
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| pslexp ss_comma pslexp_comma_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

exp_comma_list:
	/* nothing */
	{ $$ =	LISTEND(0); }
| exp
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| exp ss_comma exp_comma_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

formal:
  sd_id { $$ = TREE2("Oformal", $1, 0); }
| sd_id ss_colon orange_node_qualifier_list { $$ = TREE2("Oformal", $1, $3); }
;

formal_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| formal
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| formal ss_comma formal_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

qexp:
  s_left ss_colon exp { $$ =
	 TREE2("Qexp", TREE1("SOME", TREE0("\"left\"")), $3);
	}
| s_right ss_colon exp { $$ =
	 TREE2("Qexp", TREE1("SOME", TREE0("\"right\"")), $3);
	}
| sd_id ss_colon exp { $$ =
	 TREE2("Qexp", TREE1("SOME", $1), $3);
	}
;

qexp_comma_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| qexp
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| qexp ss_comma qexp_comma_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

sd_id_comma_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| sd_id
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| exp ss_comma sd_id_comma_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

orange_node_qualifier_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| orange_node_qualifier orange_node_qualifier_list
	{ $$ =
	LISTCONS($1, $2);
	}
;

orange_instance_qualified_list:
 orange_instance_qualified 
	{ $$ =
	LISTCONS($1, LISTEND(0));
	}
| orange_instance_qualified ss_comma orange_instance_qualified_list
	{ $$ =
	LISTCONS($1, $3);
	}
;

h2_imp_list:
	/* nothing */
	{ $$ =
	LISTEND(0);
	}
| h2_imp h2_imp_list
	{ $$ =
	LISTCONS($1, $2);
	}
;
 
h2_imp:
  sd_id ss_colon 
	{ $$ =
	TREE1("Olabel", $1);
	}

| exp exp ss_semicolon
	{ $$ =
	TREE1("Oe_as_c", $1);
	}

| exp ss_pling exp ss_semicolon
	{ $$ =
	TREE2("Ochannel_write", $1, $3);
	}

/* Unqualified play occurrence statements are parsed as e_as_c */
| exp ss_semicolon
	{ $$ =
	TREE1("Oe_as_c", $1);
	}

| s_goto sd_id ss_semicolon
	{ $$ =
	TREE1("Ogoto", $2);
	}

| ss_lsect  h2_imp_list ss_rsect // imp block
	{ $$ =
	TREE1("Oblock", $2);
	}

| exp ss_colonequals exp ss_semicolon  { $$ = TREE2("Ocolonassign", $1, $3);	}


| s_break ss_semicolon
	{ $$ =
	TREE0("Obreak");
	}

| s_continue ss_semicolon
	{ $$ =
	TREE0("Ocontinue");
	}

| s_waituntil ss_lpar exp ss_rpar ss_semicolon
	{ $$ =
	TREE1("Owaituntil", $3);
	}

| s_wait ss_lpar exp ss_rpar ss_semicolon
	{ $$ =
	TREE1("Owait", $3);
	}


| s_guard ss_lpar exp ss_rpar h2_imp 
	{ $$ =
	TREE2("Oguard", $3, $5);
	}


|  s_play h2_imp  { $$ = 
	OBEV_LINEPOINT(TREE3("Oplay", TREE0("NONE"), TREE0("NONE"), $2));
	}

|  s_play sd_id ss_colon h2_imp  { $$ = 
	OBEV_LINEPOINT(TREE3("Oplay", TREE1("SOME", $2), TREE0("NONE"), $4));
	}

|  s_play sd_id Oh2_formals ss_colon h2_imp  { $$ = 
	OBEV_LINEPOINT(TREE3("Oplay", TREE1("SOME", $2), TREE1("SOME", $3), $5));
	}


| s_if ss_lpar exp ss_rpar h2_imp 
	{ $$ =
	TREE3("Oif", $3, $5, TREE0("NONE"));
	}

| s_if ss_lpar exp ss_rpar h2_imp s_else h2_imp
	{ $$ =
	TREE3("Oif", $3, $5, TREE1("SOME", $7));
	}

| s_return exp ss_semicolon
	{ $$ =
	TREE1("Oresultis", $2);
	}

| s_while ss_lpar exp ss_rpar h2_imp
	{ $$ =
	TREE2("Owhile", $3, $5);
	}

| s_arb exp_comma_list ss_semicolon
	{ $$ =
	TREE1("Oarb", $2);
	}

| s_for ss_lpar h2_imp exp2 ss_semicolon exp ss_rpar h2_imp
	{ $$ =
	TREE4("Ofor", $3, $4, $6, $8);
	}

| s_forever h2_imp
	{ $$ =
	TREE1("Oforever", $2);
	}
;
 

exp:
  exp1 { $$ = $1; }

| qexp  { $$ = $1; }

| exp1 ss_equals exp1 
	{ $$ =
	TREE3("Oassign", TREE0("NONE"), $1, $3);
	}
| exp1 ss_plusequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Oplus")), $1, $3);
	}
| exp1 ss_rshiftequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Orshift")), $1, $3);
	}
| exp1 ss_lshiftequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Olshift")), $1, $3);
	}
| exp1 ss_dividequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Odivide")), $1, $3);
	}
| exp1 ss_timesequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Otimes")), $1, $3);
	}
| exp1 ss_minusequals exp1 
	{ $$ =
	TREE3("Oassign", TREE1("SOME", YYLEAF("Ominus")), $1, $3);
	}

;


exp1:
  exp2	{ $$ = $1; }
| exp2 ss_query exp2 ss_colon  exp1 { $$ = TREE3("Oquery", $1, $3, $5); }
;

exp2:
  exp3	{ $$ = $1; }

| exp3 ss_rarrow2 exp3	{ $$ = 
	TREE3("Odiadic", YYLEAF("Oimplies"), $1, $3); 
	}
;


exp3:
  exp4	{ $$ = $1; }
;


exp4:
  exp5	{ $$ = $1; }
| exp4 ss_logor exp5	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ologor"), $1, $3); 
	}
| exp4 ss_disj exp5	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ologor"), $1, $3); 
	}
;


exp5:
  exp6	{ $$ = $1; }
| exp5 ss_logand exp6	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ologand"), $1, $3); 
	}
| exp5 ss_caret exp6	{ $$ = 
	TREE3("Odiadic", YYLEAF("Oxor"), $1, $3); 
	}
| exp5 ss_conj exp6	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ologand"), $1, $3); 
	}
;

exp6:
  exp65	{ $$ = $1; }

| exp65 ss_deqd exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odeqd"), $1, $3); 
	}
| exp65 ss_dned exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odned"), $1, $3); 
	}
| exp65 ss_dltd exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odltd"), $1, $3); 
	}
| exp65 ss_dled exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odled"), $1, $3); 
	}

/* Reversed operators: */
| exp65 ss_dged exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odled"), $3, $1); 
	}
| exp65 ss_dgtd exp65	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odltd"), $3, $1); 
	}
;



exp65:
  exp7	{ $$ = $1; }
| exp7 ss_lshift exp7	{ $$ = 
	TREE3("Odiadic", YYLEAF("Olshift"), $1, $3); 
	}
| exp7 ss_rshift exp7	{ $$ = 
	TREE3("Odiadic", YYLEAF("Orshift"), $1, $3); 
	}
;

exp7:
  exp8	{ $$ = $1; }
| exp8 ss_stile exp7	{ $$ = 
	TREE3("Odiadic", YYLEAF("Obinor"), $1, $3); 
	}

| exp7 ss_plus exp8	{ $$ = 
	TREE3("Odiadic", YYLEAF("Oplus"), $1, $3); 
	}

| exp7 ss_minus exp8	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ominus"), $1, $3); 
	}


;

exp8:
  exp9	{ $$ = $1; }
| exp8 ss_ampersand exp9	{ $$ = 
	TREE3("Odiadic", YYLEAF("Obitand"), $1, $3); 
	}
| exp8 ss_slash exp9	{ $$ = 
	TREE3("Odiadic", YYLEAF("Odivide"), $1, $3); 
	}
| exp8 ss_star exp9	{ $$ = 
	TREE3("Odiadic", YYLEAF("Otimes"), $1, $3); 
	}
| exp8 ss_star2 exp9	{ $$ = 
	TREE3("Odiadic", YYLEAF("Oexp"), $1, $3); 
	}

;

exp9:
  exp10	{ $$ = $1; }
;


exp10:
/* */  exp11	{ $$ = $1; }

| s_rose exp11	{ $$ = TREE2("Opsl_builtin", mkstring("rose"), $2); }
| s_fell exp11	{ $$ = TREE2("Opsl_builtin", mkstring("fell"), $2); }
| s_stable exp11	{ $$ = TREE2("Opsl_builtin", mkstring("stable"), $2); }
| s_next exp11	{ $$ = TREE2("Opsl_builtin", mkstring("next"), $2); }
| s_prev exp11	{ $$ = TREE2("Opsl_builtin", mkstring("prev"), $2); }

;

exp11:
  exp12	{ $$ = $1; }
;

exp12:
  exp13	{ $$ = $1; }
;


exp13a:
  sd_id { $$ =
	TREE1("Oid", $1);
	}

| sd_id ss_dot exp13a	{ $$ = 
	TREE3("Odiadic", YYLEAF("Ocatenate"), TREE1("Oid", $1), $3); 
	}

;


tnumber_list:
  sd_number { $$ = TREE1("Otnumber_end", TREE0($1 < 0 ?  "true": "false")); }
| sd_tnumber tnumber_list { $$ = TREE2("Otnumber", $1, $2);	}
;


exp13:
  exp13a ss_lpar exp_comma_list ss_rpar
    { $$ =
	TREE2("Oapply", $1, $3);
    }

| exp13a ss_lbra  exp ss_colon exp ss_rbra 
    { $$ =
	TREE3("Oexp_range", $1, $3, $5);
    }

| exp13a ss_lbra  exp ss_rbra 
    { $$ =
	TREE2("Oexp_subsc", $1, $3);
    }


| exp13a { $$ = $1; }

| ss_lpar exp ss_rpar { $$ = $2; }

| ss_query exp13
    { $$ =
	TREE1("Ochannel_read", $2);
	}


| sd_tnumber tnumber_list { $$=TREE2("Cil_tnumber", $1, $2);	}

| sd_number
    { $$ =
	TREE1("Onum", $1);
	}

| sd_string
    { $$ =
	TREE1("Ostring", $1);
	}

| ss_tilda exp13
	{ $$ =
	TREE1("Obinnot", $2);
	}

| ss_pling exp13
	{ $$ =
	TREE1("Olognot", $2);
	}
;

%%

#include <stdio.h>
#include <ctype.h>

#include "lineno.h"


extern FILE *stderr;

int yyerror (const char *s) 
{
	extern void cleanexit(int);	
  extern builder *lishlex();
	int line_number = filestack[filesp].line_number;
	char *fn = filestack[filesp].fn;
    fprintf(stderr, "Syntax error: %s: %s:; %i\n", s, fn, line_number);
		fprintf(stderr, "Next symbol: %s\n", atom_to_str(lishlex()));
	cleanexit(1);
		return 1;

}


void yydebug_on()
{
#ifdef YYDEBUG
	yydebug = 0;
#endif
}

char *smllib = "h2gram";
int g_need_ee_starter = 0;

/*
 * Two characters which define the escape seq for comment to end of line 
 */
char commentchar1 = '/';
char commentchar2 = '/';
char *langsuffix = ".h2";


int yylex()
{
  char s;  int v;
  extern builder *lishlex();
  extern int lextracef;
#ifdef CBG_YYDEBUG
  yydebug=1;
#endif

  builder *b, *a = lishlex();

  if (!a) return 0;
  yylval.auxval = a;

  if (fnumberp(a)) return sd_number;
  else if (fstringp(a)) return sd_string;
  else if (ftopnumberp(a)) 
	{
	if (lextracef)  printf("Lex of multi-digit number %i 0x%x\n", atom_to_int(a), atom_to_int(a)); fflush(stdout);
	return sd_tnumber;
	}

  b = fgetprop(a, smacro);
  if (lextracef)  printf("%i Lex %i %p |%s|\n", 0, v, a, 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;
  cbgerror(cbge_fatal, "Illegal input token %c", s);
  return 0;
}




/* eof */

Abstract syntax tree

The H2 HPR abstract syntax tree is defined using the following SML datatype:

(*
 *  $Id: h2gram.sml,v 1.14 2008/09/27 08:14:07 djg11 Exp $
 *
 * Bigtop.  
 * (C) 2003 DJ Greaves. All rights reserved.
 * www.orangepath.com
 *
 * H2 is a member of the Orange series of experimental languages, hence the naming conventions.
 *
 *)

open linepoint_hdr;

datatype metainfo_t = 
  MIA of string * string
| MIA_filler
;



datatype Odiop_t = Oand | Oor | Obiimp | Oimplies | Ointerm | Obitand | Ologand | Obitor | Ologor | Oxor | Odeqd | Odned | Ocatenate | Odiadic_msg_stopper | Obinor | Oplus | Ominus | Otimes | Omod | Odivide | Odltd | Odled | Olshift | Orshift | Oexp
; 



datatype Oquantif_t = Ouniv | Oexists
;

datatype Ovarmode_t = O_INPUT | O_OUTPUT | O_INOUT;

datatype Ohand_t = h2_left | h2_right;

(* A transitioner should be one of entry | body | exit *)
type Oh2_transitioner_t = string;  



datatype oexp_t = 
        Odiadic of Odiop_t * oexp_t * oexp_t
|       Oquery of oexp_t * oexp_t * oexp_t
|       Oassign of Odiop_t option * oexp_t * oexp_t 
|       Obinnot of oexp_t
|       Oheir of oexp_t list
|       Oexp_range of oexp_t * oexp_t * oexp_t
|       Ochannel_read of oexp_t
|       Olognot of oexp_t
|       Oid of string
|       Opsl_builtin of string * oexp_t
|       Odot of oexp_t * string
|       Onet of string 
|       Ostring of string
|       Otrue | Ofalse | Ounit | Oundef
|       Onum of int
|       Oiodecl of string * int * int * Ovarmode_t
|       Oapply of oexp_t * oexp_t list
|       Oapply1 of oexp_t * (Oformal_t list * obev_t list) * oexp_t list
|       Oquantif of Oquantif_t * oexp_t
|       Ovalof of obev_t
|       Oexp_subsc of oexp_t * oexp_t
|       Qexp of string option * oexp_t
      
and obev_t = 
   Olabel of string
|  Oskip
|  Obreak
|  Ocontinue
|  Ocolonassign of oexp_t * oexp_t
|  Oguard of oexp_t * obev_t
|  Owait of oexp_t
|  Owaituntil of oexp_t
|  Oif of oexp_t * obev_t * obev_t option
|  Owhile of oexp_t * obev_t
|  Oarb of oexp_t list
|  Oforever of obev_t
|  Ofor of obev_t * oexp_t * oexp_t * obev_t
|  Oblock of obev_t list
|  Oplay_occurrence of Ohand_t * oexp_t list option * oexp_t
|  Ogoto of string
|  Oe_as_c of oexp_t
|  Ochannel_write of oexp_t * oexp_t
|  Obev_linepoint of linepoint_t  * obev_t
|  Oplay of string option * oexp_t list option * obev_t
|  Oresultis of oexp_t

and Oformal_t = Oformal of string * Onode_decl_nq_t list

and  Ounit_mode_t = Oprotocol | Osection | Ointerface | Ounitmode | Oentity | Oaction | Otype
 

and temporal_t = Oinitial | Oalways | Oidle | Onever | Ofair


and Orange_presence_t = Ounit_presence of Ounit_mode_t * string * Oformal_t list *Ounit_facet_t list
  | Ounit_typedef of string * Ounit_facet_t
  | Ounit_msg_stopper


and Oui_t = Oui of string * oexp_t list

and pslc_t = 
	  Pslc_plus 
	| Pslc_goto 
	| Pslc1 of oexp_t * string
	| pslc_o2 of oexp_t

and pslexp_t = 
    Psl_leaf of oexp_t
|   Psl_diadic of string * pslexp_t * pslexp_t
|   Psl_rep1 of pslexp_t * pslc_t 
|   Psl_rep2 of pslexp_t * pslc_t * pslc_t

and Ounit_facet_t = 
   Oui_instance of Ounit_mode_t * string * Oui_t list

	(* Types are a subtype of facets. *)
|  Ot_enum of string list
|  Ot_bool
|  Ot_natural 
|  Ot_int
|  Oui_forward
|  Oui_reverse
|  Oui_neutral
|  Oui_const of string * oexp_t 
|  Oui_connect of string option * oexp_t list * obev_t list
|  Oui_node_decl of Onode_decl_nq_t list * Oiq_t list
|  Oui_stategraph of string * string list * Oh2_state_t list
|  Oui_statevar_decl of string * Ounit_facet_t (* TODO any type now *)
|  Oui_bev of oexp_t option * obev_t list
|  Oui_bevplus of Ounit_facet_t * Ounit_facet_t
|  Oui_temporal of temporal_t * pslexp_t list
|  Oui_colonassign of oexp_t * oexp_t
|  Oui_linepoint of linepoint_t * Ounit_facet_t
|  Oui_fundef of string * Oformal_t list * obev_t list

and Oh2_state_t =
        Oh2_state_def of string * oexp_t list list * Oh2_stateitem_t list

and Oh2_stateitem_t =
        Oh2_transition of Oh2_statespec_t * Oh2_statespec_t * obev_t option
|       Oh2_state_action of Oh2_transitioner_t * obev_t

and Oh2_statespec_t =
        Oh2_state_exp of oexp_t
|       Oh2_exit_state_exit
|       Oh2_exit_state_tagged_exit of string

and Oiq_t =
   Oiq_pling of string * oexp_t list
|  Oiq_id of string * oexp_t list

and Onode_decl_nq_t =
   Onq_out
|  Onq_in
|  Onq_target
|  Onq_initiator
|  Onq_integer
|  Onq_forward
|  Onq_reverse
|  Onq_neutral
|  Onq_inverted
|  Onq_inout
|  Onq_user of string
|  Onq_dimension of oexp_t
|  Onq_square_range of oexp_t * oexp_t
|  Onq_dot_range of oexp_t * oexp_t
|  Onq_bit of Ounit_facet_t (* types: bit, bool, natural ... *)
|  Onq_inherit of Ounit_mode_t * string (* deprecate - use node instead *)
|  Onq_channel
|  Onq_event
|  Onq_mutex
|  Onq_value
|  Onq_parameter
|  Onq_enum of string list
|  Onq_init of oexp_t
|  Onq_reg
|  Onq_unsigned
|  Onq_signed
|  Onq_port of string
|  Onq_undefrange
;


datatype h2_decl = 
  Osimplebev of string list * obev_t list;
   

(* eof *)


H2 Types

All expressions either have integer type or else denote partial types that are eliminated during an elaboration phase of compilation, such as channel names, parameters and module instance names.

The boolean type is represented by the integer subrange 0..1;

Type expressions are a type name, an enumeration, an integer range or a vector range.

An integer range is two integers separated by two dots, such as ` 0..1'. The first number is, by convention, lower than the second, but the order is ignored.

A Verilog RTL style vector range is two integers in brackets separated by a colon, such as `[7:0]'. This example defines an integer range of 0..255 and names the bits of a bus representation of the integer.

An array type is denoted with square brackets and if the length of the array is known, this is placed in the brackets. The subscript range of the array is from zero to the number in brackets minus one.

An enumeration type is a set of constant strings. It is defined in braces, prefixed with the keyword enum. For example

   enum { Play, Forward, Stop, Reverse }

All enumeration constants must be disjoint within their scope of use.

Note: stategraphs implicitly define enumerations with their state names.

Type names can be established with the typedef statement. For example

   typedef safe_range_t = -55..55;
   typedef transport_t = enum { Play, Forward, Stop, Reverse };


H2 Expressions

H2 Constant Expressions

The following constants are builtin: X, (?), true, false. The symbol 'X' denotes don't care.

Any sequence of digits is a base-ten integer, and such integers can start with a minus sign.

H2 Variables, Events and Parameters

Variables are defined using the node statement, or one of its shorthand forms (§1.6.2).

Variables have three basic types: parameter, value or event. A value or parameter variable ranges over a finite range of integers and where this is just the range 0..1 we call it a boolean variable. An event variable ranges of any finite enumeration but also possesses the property of not currently occurring, which may be thought of as an extra value. Another type is the mutex, which is a special form of boolean value type with special properties.

All variables have a scope that is the facet they are defined in and all facets directly instantiated below, unless textually masked by more closely enclosing declarations.

Access between facets is enabled using path names consisting of a facet instance names separated by dots.

An facet definition may contain a list of structural formal parameters in parenthesis after its name. These are formal parameters to the facet and are expanded at instantiation using call by name. They are used only for structural (macro-style) elaboration and are not user variables.

All parameter variables must be eliminated during compilation through not being needed or by being given a constant value, either specified by the user or chosen by the compiler.

Operator Expressions

The symbol 'X', when standing along, denotes don't care. When used as a function it denotes the next state operator. The expressions $X(e)$ is short for $X(e, 1)$ and means the next value of expressions $e$. Higher values of $n$ in $X(e, n)$ denote further values into the future, using the expansion $X(e, n+1) = X(X(e, n))$.

Bit extract is denoted with brackets: eg. `e[e]'.

The diadic pling operator, `c!e', writes a value to a named channel. The expansion of channel writes is explained in §1.4.

Function Application

Function applications are either of built-in functions or of user functions that act as macros and are expanded at compile time.

The built-in function 'pause()' is used to denote a bus-settling delay or memory-barrier. By calling this function, the current thread is bocked until all writes made to variables or nets are flushed out and made visible to other processes. It should always be given the argument 1.

The built-in function 'hpr_testandset(mutex, bool)' must take a variable of type mutex (a boolean subtype of value) as its first argument. If the second argument is 'true' then the function attempts to set the mutex and returns the previous value. If the second argument is 'false' then the mutex is cleared and false is returned.

The built-in function 'print()' causes console output under simulation or on an embedded platform if supported. The arguments are converted to an ASCII representation and output in turn.

The built-in function 'exit(rc, [msg ...])' causes a simulation to exit. An error is indicated using a non-zero return code in the first argument. Supporting message information may also be provided in subsequent arguments. The behaviour on embedded platforms, if supported, is to halt execution of all threads until a reset occurs.

The built-in function 'X' is explained in§1.2.3.

User-defined functions are declared with the fundef keyword.


H2 Assertions

An assertion statement constrains the behaviour of the system.

The assertion statements may be free standing, or may be used in the C-like code or in the action section of a statecharts.

Where free standing, they must universally hold.

Only the safety assertions and fairness marker can occur in the C-like code and statecharts. Their meaning is then respectively guarded by the C-like thread reaching them or the state being active.

Assertions refering to events and patterns of events follow the syntax and semantics follows PSL: [[`Property Specification Language Reference Manual' Version 1.1 June 9, 2004]

   assertion ::=
       always   [ <string> : ] <pslexp>; 
   |   never    [ <string> : ] <pslexp>; 
   |   initial  [ <string> : ] <pslexp>; 
   |   live     [ <string> : ] <pslexp>; 
   |   fair     [ <string> : ] <pslexp>;


H2 Channels

The compiler implements message passing channels. The pling operator is used to put a value to a channel and the query operator is used for reading from a channel. Both are blocking operators, because channels implement reliable flow-control.

The channel operations may be used in the C-like code or in the action section of a statecharts. A blocking channel operation in a statechart will make the whole of/part of the state machine block (TODO explain).

The current implementation of channels is via straightforward macro expansion in the front end of the compiler. Channels are implemented by shared access to entries in an array called C

Both operators make copies of the channel designator on entry, in case the user's expression should change while blocked, and the write operator makes a copy of the value to be sent. Copies are not made for manifest constant expressions. Copies are kept in fresh variables denoted below with the `_c' suffix. The allocation of index values to the array is handled by the compiler, and the back-end compilation phase replaces hardware constant indexes with scalars.

The expansion of the write operation $c!e$ is

  c_c = c;
  e_c = e;
  waituntil !C.ack[c_c];
  C.data[c_c] = e_c;
  C.req[c_c] = 1;
  waituntil C.ack[c_c];
  C.req[c_c] = 0;

The expansion of the read operation $?c$ is

  c_c = c;
  waituntil C.req[c_c];
  r_c = C.data[c_c];
  C.ack[c_c] = 1;
  waituntil !C.req[c_c];
  C.ack[c_c] = 0;
  return r_c;


H2 C-like Imperative Statements

The H2 language possesses various subsets. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts. This section defines the C-like imperative subset.

H2 includes a typical block-structured imperative programming language with semantics based on those of C, but extended with operators including channel write and the `guard' statement.


The H2 if statement

   if (<exp>) <statment>
   if (<exp>) <statment> else <statment>

The H2 if statement executes its argument if the condition evaluates to a non-zero value.


The H2 while statement

   while (<exp>) <statment>

The H2 while statement evaluates its body while its argument evaluates to a non-zero value.


The H2 emit statement

   emit  <var>;

The H2 emit statement sends a nullary event to a named variable that must be an event variable. Parameterised events are not generated using this statment. Instead they are generated by assigning values to the event variable.


The H2 waituntil statement

   wait (<exp>);

The H2 waituntil statement takes an expression and blocks a thread until the expression would evaluate to a non-zero value.


The H2 wait statement

   wait (<exp>);

The H2 wait statement takes a postive numeric argument and blocks a thread for that number of time units.


The H2 guard statement

   guard (<exp>) <statment>

The H2 guard statement evaluates its body if the guard expression gives a non-zero value, but the thread exits immediately from the body if the guard expression becomes zero at any time during the execution of the body, whether the thread is blocked or not.


The H2 resultis statement

   resultis (<exp>);
The H2 resultis statement returns a value to a surrounding context. It is intended to be used with the valof operator. It is interchangeable with the return statement.


The H2 return statement

   return <exp>;
The H2 return statement returns a value to a surrounding context. It is intended to be used in function bodies. It is interchangeable with the resultis statement.


The H2 skip statement

   skip;

The H2 skip statement does nothing.


The H2 continue statement

   continue;

The H2 continue statement transfers execution to the head of the innermost surrounding while or for loop.

The H2 break statement

   break;

The H2 break statement transfers execution to the exit point of the innermost surrounding while or for loop.

The H2 label statement

    L:

The label statement defines a target for a goto statement.


The H2 goto statement

.
   goto L;

The H2 goto statement transfers execution to the named label which must be present somewhere in the same behavioural sequence.

The H2 block statement

.
   { S1 S2 .... Snnn }

The H2 block statement consists of any number of statements enclosed inside braces and they are executed in sequence.

The H2 assignment statement

. .
   <variable> = <exp>;

The H2 assignment statement assigns a value to a variable. The assignment is actually an expression and any expression can be used in this context. A function call expression becomes a procedure call in this way.

The H2 procedure call statement

.
   <name>(<arg1>, ...);

The H2 procedure call statement executes a procedure, including certain builtin procedures (§1.2.4). The call is actually an expression and any expression can be used in this context. A function call expression becomes a procedure call in this way.

The H2 channel write statement

.
   <channel> ! <exp>;

The H2 channel write statement evaluates an expression and writes the value to a named channel. The expression is evaluated immediately but the thread can then become blocked if the is not ready to read.


H2 Structural Statements

The H2 language possesses various subsets. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts. This section defines the structural subset.

The structural statements in H2 are unlike those in most languages. The power of H2 is in its structural statements.


Facet definitions

An H2 program consists of a number of facet definitions. A facet definition includes instances of other facets and local code. Facet definitions may be builtin, loaded from libraries or user defined. An instance of a facet is commonly called a node and the node statement, or a shorthand for it, is used to instantiate all facets, except for the topmost facet. The topmost facet is instead mentioned on the command line and is called the root.

The facet declaration syntax is:

   structural_item ::=  
        <directional_context> |
        <node_declaration> |
        <constant_defintion> |  
        <behavioural_section> | 
        <statechart> | 
        <connect_statement> |
        <assertion>

   facet_definition ::= 
      <facet_type> <facet_name>  [ (<structural_formal>, ... ) ]
      {
         [ <structural_item> ... ]
      }

   structural_formal ::= <id>

The facet_type must (currently) be one of the builtin facet types: section, unit, protocol or interface.

The facet_name must be a fresh identifier.

The structural formal parameters are optional, but must all be provided with values whenever the facet is instantiated. They bind identifiers occurring in the facet and there is almost no restriction over the connect of the identifiers (e.g. types, facet names, constants etc.). Currently, the topmost facet cannot have formals since it is instantiated from the command line.

The contents of the facet are structural items defined in the rest of this section.

H2 defines a number of builtin leaf facets: node, protocol, action, section, interface and section. The node is the most general facet and also the most basic: a node can be as simple as a boolean variable, but it can be any other variable, channel or facet. The user defines his own facets that inherit from one of these. Facets are heirarchic, in that each may instantiate further, lower facets. Each instantiation may be forwards or reversed and inverted or not.


Node declaration statement

The H2 node statement declares

   node_declaration ::=
       node    <node_type> [ <modifier> ... ] : <nid> [ , <nid> ... ];

   nid ::=  <id> | !<id> | <id> (<exp> [, <exp> ... ])
   node_type ::= <id>

The node statement creates one or more named instances of an facet. The names must be disjoint. Every node has a type. The type name can be used instead of the keyword `node' where the type is one of these builtin facet types: channel, event, mutex, parameter, section, protocol, action, unit or interface.

When nodes are instantiated, modifiers may be used. The available modifiers are: out, in, inout, event, unsigned, , signed, channel, parameter, initiator, target, forward , reverse and range declarations for arrays and scalars of fixed ranges.

Nodes may be declared as inverted and/or reversed. An inverted declaration is made by placing the pling character before the identifier. A reversed declaration is made by inserting the reverse modifier in the modifier list. Nodes may be parameterised by supplying one or more arguments after the identifier. The number of expressions must match the number of formal parameters in the node type definition.

The program is elaborated in the textual order it occurs in the file. All identifiers ultimately form a single, flat name space. At any point in the file, all identifiers already defined through being a facet directly or indirectly instantiated in the current facet are in scope. Multiple identifiers of the same name may be in scope at once: e.g. when there are two instances of a given sort of interface. Where multiple identifiers of the same name are in scope at once, it is an error to refer to one of the multiply-defined identifiers in an ambiguous way. Sufficient facet prefix path details must be supplied.


Range and Array modifiers

A modifier of the form [ n .. m ] defines a node that can take on an integer range of values.

A modifier of the form [ h : l ] defines a packed vector node with high and low bit positions called h and l. This is another way of defining a range. A value of zero is normally used for l.

A modifier of the form [ n ] defines an array with n locations, indexed from zero.

A modifier of the form [ ] defines an array with an unbounded number of locations.

Only one of the first two forms is allowed for a given node.


Forwards, Reverse and Neutral modifiers

   directional_context ::= forward: | neutral: | reverse:

When connecting a pair of components, the inputs of one component are normally connected to outputs of the other, and vice versa. This requires that these terms must be reversed when a specification written for one side of the interface is being used at the other. This is known as having a handed pair. To overcome this issue, when any type of node is declared/instantiated, including interface nodes and complete sections, it is defined in a directional context. A reverse context causes inputs to be interpreted as output and outputs to be interpreted as inputs.

The default directional context is forward, but neutral and reverse contexts also exist. The current directional context is altered to the desired value by the forward:, reverse: and neutral: labels. These labels alter the current context in the textually following declarations until another label is encountered. In addition, the first two of these three words may also appear as a modifier in the actual declaration of the node. The overall context of a node is reverse if there is an odd number of reversings in the referring path. A path is reversed by each reverse instantiation. A reverse instantiation either contains the reverse keyword as a modifier or is inside a reverse directional context, but not both. If it both, they cancel out. Declarations inside a neutral directional context are not altered and have their default meaning regardless of how many reversings there are on the referring path.


Temporal Regular Expressions

The H2 language possesses various subsets. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts. This section defines the temporal logic (PSL) definitions.

TODO. Contents of this section are missing, but are mainly bog standard PSL.


Stategraph Definition

The H2 language possesses various subsets. The main subsets are structural, temporal logic (PSL), C-like imperative and sysML-like state hierarchic charts. This section defines the statechart subset.

The stategraph (or statechart) 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 abort: // A special state that can be 
                  // forced remotely (also called disable).
	
   ...

}

A state may contain tagged statements, 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 abort may be disabled from elsewhere in the same bundle using the `abort' statement. Please see §1.8.1.

The stategraph general form is sufficient to encompass the SysML state machines.


Abort Statement

The `abort' statement is used for a remote abort of a stategraph.

Syntax:

  if (g) abort stategraph_name1, stategraph_name2, ...;

The abort statement must be conditional, otherwise the stategraph would never leave its abort state, and the abort guard, $g$ may either be an event or level expression. When the abort guard is a level expression it takes precedence over any transitions in the stategraph that lead from the abort state.

  if (g) abort stategraph_name1, stategraph_name2, ...;


next up previous index
Next: Joining Automata Synthesis Up: SPL Orangepath H2 Language Previous: SPL Orangepath H2 Language   Index
David Greaves 2009-08-20