.Open Table 2: Structured English Grammar - Natural Language
. Source
.See [Grunske08]
. Start
probabilisticProperty ::= "The system shall have a behavior where" $patternStateFormula.
. ProProST Pattern
patternStateFormula ::= "with a probability" $probabilityBound "it is the case that"  $occurenceStateFormula| $orderStateFormula.
occurenceStateFormula ::= $transientStateProbability | $steadyStateProbability | $probabilisticInvariance | $probabilisticExistence.
orderStateFormula ::= $probabilisticUntil | $probabilisticPrecedence | $probabilisticResponse | $probabilisticConstResponse.
transientStateProbability ::= $stateFormula "holds after exactly" $time "time units.".
steadyStateProbability ::= $stateFormula "holds in the long run.".
probabilisticInvariance ::= $stateFormula "holds continuously" $timeBound ".".
probabilisticExistence ::= $stateFormula "will eventually hold" $timeBound ".".
probabilisticUntil ::= $stateFormula2 "holds" $timeBound "after" $stateFormula1 "has held continuously before".
probabilisticPrecedence ::= $stateFormula2 "holds before" $stateFormula1 "can hold" $timeBound ".".
probabilisticResponse ::= "if" $stateFormula1 "holds, then as a response" $stateFormula2  "becomes true" $timeBound ".".
probabilisticConstResponse ::= "if" $stateFormula1 "holds, then as a response" $stateFormula3 "becomes true" $timeBound "without" $stateFormula2"holding in between.".
. Time
timeBound ::= $noTimeBound | $upperTimeBound | $lowerTimeBound | $timeInterval.
noTimeBound ::= "".
upperTimeBound ::= "within" $time "time units".
lowerTimeBound ::= "after" $time "time units".
timeInterval ::= "between" $time  "and" $time "time units".
time::=Positive & Real.
. Probability
probabilityBound ::= $lowerProbBound | $lowerOrEqualProbBound | $higherProbBound| $higherOrEqualProbBound.
lowerProbBound ::= "lower than" $probability.
lowerOrEqualProbBound ::= "lower or equal than" $probability.
higherProbBound ::= "greater than" $probability.
higherOrEqualProbBound ::= "greater or equal than" $probability.
probability::=[0..1].
. Final
SimpleStateProperty::=given.
stateFormula ::= SimpleStateProperty.
stateFormula1 ::= SimpleStateProperty.
stateFormula2 ::= SimpleStateProperty.
stateFormula3 ::= SimpleStateProperty.
.Close