https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> Correct some typos and add things to do. * src/str/prism-desugar.str: Correct a typo (thanks vimspell). * src/str/eval-meta-code.str: Ditto. * src/syn/prism/PRISM-Command.sdf: Ditto. * src/syn/xrm/XRM-Command.sdf: New. Seems to be broken. * src/syn/xrm/XRM-Main.sdf: Import XRM-Command. * TODO: Add a couple of nice ideas suggested by Michael Cadilhac. Update things done. TODO | 90 +++++++++++++++++++++++++--------------- src/str/eval-meta-code.str | 2 src/str/prism-desugar.str | 2 src/syn/prism/PRISM-Command.sdf | 2 src/syn/xrm/XRM-Command.sdf | 11 ++++ src/syn/xrm/XRM-Main.sdf | 1 6 files changed, 72 insertions(+), 36 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 29) +++ src/str/prism-desugar.str (working copy) @@ -48,7 +48,7 @@ rules /** - ** Remove conditionnal updates. + ** Remove conditional updates. ** [] guard -> unconditionnal-update-list; ** is rewritten as: ** [] guard -> 1:(unconditionnal-update-list); Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 29) +++ src/str/eval-meta-code.str (working copy) @@ -37,7 +37,7 @@ <eval-meta-code> else-part else ice(|"eval-meta-code", <concat-strings> [ - "the conditionnal test of a meta if could ", + "the conditional test of a meta if could ", "not be reduced to a single value (True or", " False), this should have been detected ", "earlier"], Index: src/syn/xrm/XRM-Command.sdf --- src/syn/xrm/XRM-Command.sdf (revision 0) +++ src/syn/xrm/XRM-Command.sdf (revision 0) @@ -0,0 +1,11 @@ +module XRM-Command +imports + PRISM-to-XRM + +exports + + %% EBNF Grammar: Extended Commands + %% Command ::= "[" ArrayAccess "]" Expression "->" Updates ";" + + context-free syntax + "[" ArrayAccess "]" Expression "->" Updates ";" -> Command {cons("Command")} Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 29) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -8,3 +8,4 @@ XRM-Literals XRM-Declaration XRM-Update + XRM-Command Index: src/syn/prism/PRISM-Command.sdf --- src/syn/prism/PRISM-Command.sdf (revision 29) +++ src/syn/prism/PRISM-Command.sdf (working copy) @@ -14,7 +14,7 @@ context-free syntax "[" Identifier? "]" Expression "->" Updates ";" -> Command {cons("Command")} - %% The follwing syntax was commented out in PRISM's parser... + %% The following syntax was commented out in PRISM's parser... %% It seems it will be used in the near future when rewards will be fully %% supported. Index: TODO --- TODO (revision 29) +++ TODO (working copy) @@ -14,35 +14,11 @@ * Write some sort of formal descriptions of the extensions offered. - * Fix the Int nodes in the static for loops (if its really necessary?) - ## ---------- ## ## Extensions ## ## ---------- ## - * Add static for loops and static if: - for i from 0 to 3 step 1 do => module sensor_0 - module sensor[i] => b_0 : [0..42] init 0; - b[i] : [0..42] init 0; => s_0_0 : [0..2] init 2; - for j from 0 to 3 do => s_0_1 : [0..4] init 2; - if j = 1 then => s_0_2 : [0..4] init 2; - s[i][j] : [0..j+3] init 2; => s_0_2 : [0..4] init 2; - else => - s[i][j] : [0..j+2] init 2; => [] s_0_0=0 -> (b_0'=b_0+1) - end => [] s_0_1=0 -> (b_0'=b_0+1) - end => [] s_0_2=0 -> (b_0'=b_0+1) - => endmodule - for j from 0 to 3 do => - [] s[i][j]=0 -> (b[i]' = b[i]+1) => module sensor_1 - end => b_1 : [0..42] init 1; - endmodule => s_1_0 : [0..2] init 2; - end => ... - - Of course, the for loops must be unroll-able statically. - Static for loops can be found: - - In between modules (that is, where we can expect a ModulesFileSection) - - In between commands (that is where we can expect a Declaration or a - Command) + * Add the following at the meta-level: - Let's have the possibility to generate other ModulesFileSection such as: o Formula o Constant @@ -50,15 +26,32 @@ o RenamedModule o SystemComp o RewardStruct - Notice: it's not necessary for Init since it seems only one Init - section is allowed. - I think it doesn't make sense to allow static if-then-else constructs - outside static for loops because, ATM, static for loops are the only way - to introduce static (meta-)variables (such as `i' and `j' in the previous - example). - Note: Issue a warning (or an error?) if we generate twice the same module - name. + * Add arrays (sugar). module varArrays <=> module varArrays + module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do + x[4] : [0..3]; => x_1 : [0..3]; <=> x[i] : [0..3]; + [] x[0]=0 -> ... => ... <=> end + endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ... + => endmodule <=> endmodule + + * Add a sanity check after xrm-front has finished to generate everything in + order to ensure that each module/var decl has a unique name. + + * Add bound checking. (extension of the previous point) + Dirty way: check that each variable is declared somewhere. + Hard way: detect and register array declarations and detect the bounds of + the array. When array expansion occurs, check that we're not + out of bounds. This can get very tricky since a variable can be + expanded BEFORE its actual declaration (especially in XRM). + + * Add conditional tests on arrays (with support for ranges): + x[5]=0 => x_5=0 + x[1..3]=0 => x_1=0 & x_2=0 & x_3=0 + (support things such as: x[1..3,6,8..9]) + + x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 + + NOTE: x[5]?=0 should be considered as an error. ## -------------- ## ## Desugarisation ## @@ -98,3 +91,34 @@ // ... [] x=3 -> ... // x=3 is impossible [] x=0 -> (x'=3) // x=3 is not in the definition range of x + + ## ---- ## + ## DONE ## + ## ---- ## + + The following work has been done but is kept here because it contains some + useful informations to be reused in the final documentation of the package. + + * Meta for loops and meta if statements: + for i from 0 to 3 step 1 do => module sensor_0 + module sensor[i] => b_0 : [0..42] init 0; + b[i] : [0..42] init 0; => s_0_0 : [0..2] init 2; + for j from 0 to 3 do => s_0_1 : [0..4] init 2; + if j = 1 then => s_0_2 : [0..4] init 2; + s[i][j] : [0..j+3] init 2; => s_0_2 : [0..4] init 2; + else => + s[i][j] : [0..j+2] init 2; => [] s_0_0=0 -> (b_0'=b_0+1) + end => [] s_0_1=0 -> (b_0'=b_0+1) + end => [] s_0_2=0 -> (b_0'=b_0+1) + => endmodule + for j from 0 to 3 do => + [] s[i][j]=0 -> (b[i]' = b[i]+1) => module sensor_1 + end => b_1 : [0..42] init 1; + endmodule => s_1_0 : [0..2] init 2; + end => ... + + Of course, the for loops must be unroll-able statically. + Meta for loops can be found: + - In between modules (that is, where we can expect a ModulesFileSection) + - In between commands (that is where we can expect a Declaration or a + Command)