Projects June 2006

projects@lrde.epita.fr

9 participants
106 discussions

Re: XRM 85: Remove an ambiguity in XRM Formulas.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > - ; (?i, ?decimals) // i="42", decimals="000000" > + ; ?(i, decimals) // i="42", decimals="000000" Mere optimization, or more mandatory?

17 years, 10 months

Re: XRM 83: Add bound checking on arrays.

by Tsuna

On 2006-06-21, SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> wrote: > * tests/xrm/rivf.xrm: Fix. > > tests/xrm/rivf.xrm | 2 +- > > 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 > Bon je sais vraiment pas ce qui se passe mais ça marche pas. J'ai essaye avec une grille 2x2 et xrm-front ne termine pas même après avoir attendu plus de 45min. Y'a forcement quelque chose qui fait que ça termine pas. Donc j'ai fait en sorte d'afficher un message a chaque fois qu'un appel a une formule paramétrée était inliné et au bout de quelques seconde je vois plus de messages... ce qui veut donc bien dire que la récursion s'arrête. Mais alors pourquoi ça continue de tourner pendant aussi longtemps? La je comprends pas... mais va falloir fixer ça rapidement. :( -- SIGOURE Benoit aka Tsuna _____ /EPITA\ Promo 2008.CSI Rock & tRoll

17 years, 10 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: 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?

17 years, 10 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.

17 years, 10 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...

17 years, 10 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.

17 years, 10 months

Re: XRM 80: Factor some code.

by Akim Demaille

Nice!

17 years, 10 months

Re: XRM 68: Extend parametrized formula to updates.

by Akim Demaille

17 years, 10 months

XRM: Urgent

by Akim Demaille

17 years, 10 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);

17 years, 10 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Projects June 2006