Projects

projects@lrde.epita.fr

1049 discussions

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: tests/pctl/man_examples.pctl > --- tests/pctl/man_examples.pctl (revision 0) > +++ tests/pctl/man_examples.pctl (revision 0) Isn't this the kind of situation where you are expected to use their parsing test suite tool?

18 years, 6 months

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: src/lib/pctl/pp/pctl-label.meta > --- src/lib/pctl/pp/pctl-label.meta (revision 0) > +++ src/lib/pctl/pp/pctl-label.meta (revision 0) > @@ -0,0 +1 @@ > +Meta([Syntax("Stratego-Box")]) ISTR that you ought to specify the start symbol to avoid bad surprises. Sure, there may be only one in your case, but let's play it safe. See Thomas who knows what to do.

18 years, 6 months

Re: XRM 82: Fix overlapping detection.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > https://svn.lrde.epita.fr/svn/xrm/trunk > Index: ChangeLog > from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> > Fix overlapping detection. > The code is getting a bit hard to follow [and maintain] probably > because it's handling many cases ... but could we make this a lot > more generic? :| I fail to understand why there are many cases...

18 years, 6 months

Re: XRM 81: Detect overlapping declarations of arrays.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > https://svn.lrde.epita.fr/svn/xrm/trunk > Index: ChangeLog > from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> > Detect overlapping declarations of arrays. > Consider the following case: > x[1][1] : [0..2] init 2; > x[1][1,2] : [0..3] init 3; > Here, we're declaring the array `x' in two parts. As we can see, the > second part overlaps with the first. Moreover the, overlapping part > has a different definition in both declarations. This is now caught > and reported as an error. Nice too.

18 years, 6 months

Re: XRM 80: Factor some code.

by Akim Demaille

Nice!

18 years, 6 months

Re: XRM 68: Extend parametrized formula to updates.

by Akim Demaille

18 years, 6 months

XRM: Urgent

by Akim Demaille

18 years, 6 months

XRM 85: Remove an ambiguity in XRM Formulas.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Remove an ambiguity in XRM Formulas. * src/str/prism-desugar.str (SimplifyDoubles): Use simple pattern matching instead of congruence with inlined strategies. * src/str/collect-static-const-decl.str: Factor some code. * src/syn/xrm/XRM-Formula.sdf: Remove an ambiguity. * tests/xrm/amb-formula.xrm: New. This was ambiguous. * tests/xrm/rivf.xrm: Rename `power' to `POWER' and `lossage' to `LOSS'. src/str/collect-static-const-decl.str | 27 +++++++++++++-------------- src/str/prism-desugar.str | 2 +- src/syn/xrm/XRM-Formula.sdf | 14 ++++++++++++-- tests/xrm/amb-formula.xrm | 3 +++ tests/xrm/rivf.xrm | 6 +++--- 5 files changed, 32 insertions(+), 20 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 84) +++ src/str/prism-desugar.str (working copy) @@ -66,7 +66,7 @@ ; string-to-real // 4.199999999999990e+01 ; real-to-string(|6) // "42.000000" ; split-at-dot // ("42", "000000") - ; (?i, ?decimals) // i="42", decimals="000000" + ; ?(i, decimals) // i="42", decimals="000000" // strcmp(decimals, "000000") == 0 ? id : fail ; !decimals => "000000" Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 84) +++ src/str/collect-static-const-decl.str (working copy) @@ -11,31 +11,30 @@ strategies - // const int - collect-static-const-decl = - ?ConstInt(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) + register-static-const(|idf, value, type) = + check-identifier-unicity(|idf) + /* NOTE: We omitted ExpandPFormulas in the following attempt to simplify + * the value before storing it in the DR because it will expand the value + * forever if it contains call to recursive parameterized formula. + */ ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("int")} => v) + ; !v'{Type(type)} => v) ; rules(ExpandStaticConsts: idf -> v) + // const int + collect-static-const-decl = + ?ConstInt(idf@Identifier(_), value) + ; register-static-const(|idf, value, "int") // const double collect-static-const-decl = ?ConstDouble(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) - ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("double")} => v) - ; rules(ExpandStaticConsts: idf -> v) - + ; register-static-const(|idf, value, "double") // const bool collect-static-const-decl = ?ConstBool(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) - ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("bool")} => v) - ; rules(ExpandStaticConsts: idf -> v) + ; register-static-const(|idf, value, "bool") strategies Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 84) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -21,10 +21,20 @@ -> FormulaDef {cons("FormulaDef")} context-free syntax - "formula" Identifier "(" {Argument ","}* ")" "=" (Expression|Update) ";" + "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" -> FormulaDef {cons("PFormulaDef")} + "formula" Identifier "(" {Argument ","}* ")" "=" Update ";" + -> FormulaDef {cons("PFormulaDef"),prefer} "formula" Identifier "=" Update ";" - -> FormulaDef {cons("FormulaDef")} + -> FormulaDef {cons("FormulaDef"),prefer} + %% We use `prefer' here for the following reason: + %% In one single case, the above rules will lead to an ambiguity + %% formula amb = parameterized_formula(...); + %% Because of the nature of PFormulaCall (see XRM-Expression) which can + %% be either an Expression or an Update, sglr will create an amb node + %% with two identical choices. This is (AFAIK) the only case which will + %% lead to an ambiguity. Since both choices are identical, we can safely + %% remove the ambiguity using a dirty `prefer'. sorts Argument context-free syntax Index: tests/xrm/amb-formula.xrm --- tests/xrm/amb-formula.xrm (revision 0) +++ tests/xrm/amb-formula.xrm (revision 0) @@ -0,0 +1,3 @@ +formula inc(int n) = n + 1; + +formula two = inc(1); Index: tests/xrm/rivf.xrm --- tests/xrm/rivf.xrm (revision 84) +++ tests/xrm/rivf.xrm (working copy) @@ -11,7 +11,7 @@ const int event_x = floor(width/2), event_y = floor(height/2); // Initial energy, percentage of lost cells. -const int power = 15, lossage = 50; +const int POWER = 15, LOSS = 50; // States. const int OFF = 0, SLEEP = 1, SENSE = 2, @@ -68,8 +68,8 @@ for y from 0 to height - 1 do module sensor[x][y] - s[x][y] : [0..4] init (static_rand (0, 100) < lossage) ? OFF : SENSE; - b[x][y] : [0..power] init power; + s[x][y] : [0..4] init (static_rand (0, 100) < LOSS) ? OFF : SENSE; + b[x][y] : [0..POWER] init POWER; [] s[x][y] = SENSE -> 1: transition (x, y, senses (x, y) ? BROADCAST : LISTEN, COST_SENSE); [] s[x][y] = LISTEN -> 1: transition (x, y, ears (x, y) ? BROADCAST : SLEEP, COST_LISTEN);

18 years, 6 months

XRM 84: Fix the type-checking traversal.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix the type-checking traversal. * src/str/type-check.str: Fix the traversal. type-check.str | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) Index: src/str/type-check.str --- src/str/type-check.str (revision 83) +++ src/str/type-check.str (working copy) @@ -33,5 +33,5 @@ check-array-access <+ Module(id, type-check) /* Because label can have array access with undefined identifiers: */ - <+ Command(id, type-check) + <+ Command(id, type-check, type-check) <+ all(type-check)

18 years, 6 months

XRM 83: Add bound checking on arrays.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add bound checking on arrays. Array accesses to undeclared arrays or out of bounds will now be caught and reported as an error. * src/str/xrm-to-prism.str: Add a type-checking pass in the main transformation pipeline. * src/str/type-check.str: New. Performs bounds checking on arrays at this time. * tests/xrm/rivf.xrm: Fix. src/str/type-check.str | 37 +++++++++++++++++++++++++++++++++++++ src/str/xrm-to-prism.str | 3 +++ tests/xrm/rivf.xrm | 2 +- 3 files changed, 41 insertions(+), 1 deletion(-) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 82) +++ src/str/xrm-to-prism.str (working copy) @@ -38,6 +38,7 @@ builtin-rand log-timed properties-in-xrm + type-check strategies @@ -97,6 +98,8 @@ end | "AST normalization (flatten-list)", 2) + ; log-timed(type-check | "Type checking", 2) + ; if <is-module-file> start-symbol then log-timed( /* get the modules that generates random numbers (XRM rand builtin) */ Index: src/str/type-check.str --- src/str/type-check.str (revision 0) +++ src/str/type-check.str (revision 0) @@ -0,0 +1,37 @@ +module type-check + +strategies + + check-array-access = + where( + (?ArrayAccess(_, _) + \ ArrayAccessPrime(a, b) -> ArrayAccess(a, b) \) + ; ?aa + ; <fetch-idf> aa => idf + ; if <DeclaredArrays> Identifier(idf) => dims-dec then + <desugar-array-access> aa => aa-list + /* for aa in aa-list, aa must be in dims-dec otherwise it's an + * out of bounds array access. */ + ; map({aa: + ?aa + ; (where(<fetch(?aa)> dims-dec) + <+ out-of-bounds-array-access(|idf, aa, dims-dec)) + }) + else + err-msg(|["Array access on an undefined array `", idf, "'"]) + ; <debug> aa + ; <xtc-exit> 5 + end + ) + + out-of-bounds-array-access(|idf, aa-list, dims-dec) = + err-msg(|["Out of bounds array access on array `", idf, "'"]) + ; <debug(!"Out of bounds subscript: ")> aa-list + ; <debug(!"Possible subscripts: ")> dims-dec + ; <xtc-exit> 5 + + type-check = + check-array-access + <+ Module(id, type-check) + /* Because label can have array access with undefined identifiers: */ + <+ Command(id, type-check) + <+ all(type-check) Index: tests/xrm/rivf.xrm --- tests/xrm/rivf.xrm (revision 82) +++ tests/xrm/rivf.xrm (working copy) @@ -100,6 +100,6 @@ properties for T from 0 to 1200 step 100 do // Alarmed triggered before instant T? - P =? [ true U (t <= 0 & true) ] + P =? [ true U (t <= T & boundary_broadcasts) ] end end

18 years, 6 months

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Projects