[Projects] XRM 61: Fix pretty-printing for PCTL/CSL.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Fix pretty-printing for PCTL/CSL. Pretty printing is now fully functional for PCTL/CSL. * src/lib/pctl/pp/pctl-label.str: Fix boxing. * src/syn/pctl/PCTL-Property.sdf: Put correct constructor names. * src/lib/pctl/pp/pctl-property.str: Ditto + take new constructor names into account. * THANKS: Typo. THANKS | 2 +- src/lib/pctl/pp/pctl-label.str | 2 +- src/lib/pctl/pp/pctl-property.str | 18 +++++++++--------- src/syn/pctl/PCTL-Property.sdf | 24 ++++++++++++------------ 4 files changed, 23 insertions(+), 23 deletions(-) Index: src/lib/pctl/pp/pctl-label.str --- src/lib/pctl/pp/pctl-label.str (revision 60) +++ src/lib/pctl/pp/pctl-label.str (working copy) @@ -4,4 +4,4 @@ // "label" "\"" Identifier "\"" "=" Expression ";" -> LabelDef prism-to-box: LabelDef(idf, exp) - -> H hs=1 [ KW["label"] "\"" ~idf "\"" "=" H hs=0 [~exp ";"] ] + -> H hs=1 [ KW["label"] H hs=0["\"" ~idf "\""] "=" H hs=0 [~exp ";"] ] Index: src/lib/pctl/pp/pctl-property.str --- src/lib/pctl/pp/pctl-property.str (revision 60) +++ src/lib/pctl/pp/pctl-property.str (working copy) @@ -60,19 +60,19 @@ -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path ~filter_ "]" ] prism-to-box: - ProbAtLeast(path, None()) + ProbMin(path, None()) -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path "]" ] prism-to-box: - ProbAtLeast(path, Some(filter_)) + ProbMin(path, Some(filter_)) -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path ~filter_ "]" ] prism-to-box: - ProbAtMost(path, None()) + ProbMax(path, None()) -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path "]" ] prism-to-box: - ProbAtMost(path, Some(filter_)) + ProbMax(path, Some(filter_)) -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path ~filter_ "]" ] /* S Operator */ @@ -160,19 +160,19 @@ -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward ~filter_ "]" ] prism-to-box: - RewardAtLeast(reward, None()) + RewardMin(reward, None()) -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward "]" ] prism-to-box: - RewardAtLeast(reward, Some(filter_)) + RewardMin(reward, Some(filter_)) -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward ~filter_ "]" ] prism-to-box: - RewardAtMost(reward, None()) + RewardMax(reward, None()) -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward "]" ] prism-to-box: - RewardAtMost(reward, Some(filter_)) + RewardMax(reward, Some(filter_)) -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward ~filter_ "]" ] /* Misc. stuff */ @@ -181,4 +181,4 @@ Init() -> H hs=0 ["\"" KW["init"] "\""] prism-to-box: - Label(s) -> H hs=0 ["\"" s "\""] + Label(idf) -> H hs=0 ["\"" ~idf "\""] Index: src/syn/pctl/PCTL-Property.sdf --- src/syn/pctl/PCTL-Property.sdf (revision 60) +++ src/syn/pctl/PCTL-Property.sdf (working copy) @@ -147,19 +147,19 @@ Expression "=>" Expression -> Property {left,cons("Implies")} Expression "=>" Property -> Property {left,cons("Implies")} Property "=>" Expression -> Property {left,cons("Implies")} - Property "|" Property -> Property {left,cons("PropOr")} - Property "&" Property -> Property {left,cons("PropAnd")} - "!" Property -> Property {cons("PropNot")} + Property "|" Property -> Property {left,cons("Or")} + Property "&" Property -> Property {left,cons("And")} + "!" Property -> Property {cons("Not")} "P" "<" Expression "[" Path Filter? "]" -> Property {cons("ProbLt")} "P" "<=" Expression "[" Path Filter? "]" -> Property {cons("ProbLtEq")} "P" ">" Expression "[" Path Filter? "]" -> Property {cons("ProbGt")} "P" ">=" Expression "[" Path Filter? "]" -> Property {cons("ProbGtEq")} "P" "=?" "[" Path Filter? "]" -> Property {cons("ProbEq")} - "P" "min" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} - "Pmin" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} - "P" "max" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} - "Pmax" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} + "P" "min" "=?" "[" Path Filter? "]" -> Property {cons("ProbMin")} + "Pmin" "=?" "[" Path Filter? "]" -> Property {cons("ProbMin")} + "P" "max" "=?" "[" Path Filter? "]" -> Property {cons("ProbMax")} + "Pmax" "=?" "[" Path Filter? "]" -> Property {cons("ProbMax")} "S" "<" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLt")} "S" "<=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLtEq")} @@ -172,14 +172,14 @@ "R" ">" Expression "[" Reward Filter? "]" -> Property {cons("RewardGt")} "R" ">=" Expression "[" Reward Filter? "]" -> Property {cons("RewardGtEq")} "R" "=?" "[" Reward Filter? "]" -> Property {cons("RewardEq")} - "R" "min" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} - "Rmin" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} - "R" "max" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} - "Rmax" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} + "R" "min" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMin")} + "Rmin" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMin")} + "R" "max" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMax")} + "Rmax" "=?" "[" Reward Filter? "]" -> Property {cons("RewardMax")} "\"init\"" -> Property {cons("Init")} "\"" Identifier "\"" -> Property {cons("Label")} - Expression -> Property {cons("Exp2Prop")} + Expression -> Property %%{cons("Exp2Prop")}%%DEBUG "(" Property ")" -> Property {bracket} context-free priorities Index: THANKS --- THANKS (revision 60) +++ THANKS (working copy) @@ -10,5 +10,5 @@ is also the one who had first suggested to have a dedicated tool to solve the problems that PRISM has, using program transformation. -Michael Cadilhac &lt;micha(a)lrde.epita.fr&gt; +Micha�l Cadilhac &lt;micha(a)lrde.epita.fr&gt; For his beta-testing, his suggestions and many (good) ideas.