AProVE Help: Probabilistic Term Rewrite Systems
Program = { "(" Decl ")" }.
Decl = "VAR" {Id} | "RULES" {Rule} | "STRATEGY" StrategyDecl | "GOAL" GoalDecl | "STARTTERM" StarttermDecl.
Rule = Term "->" TermDistWithNum | Term "->" TermDistWithProb.
TermDist = int ":" term | int ":" term "||" TermDist.
TermDistWithProb = prob ":" term | prob ":" term "||" TermDistWithProb.
Term = Id.
prob = int "/" int.
StrategyDecl = INNERMOST.
GoalDecl = TERMINATION | AST | PAST.
StarttermDecl = BASIC | ALL.
Id are non-empty sequences of characters except space,
'(', ')', '"', ':' and ',' and
excluding special sequences '->', '==',
'-><-', '|', '||'
and keywords INNERMOST, RULES,
STRATEGY, GOAL, TERMINATION, AST, PAST,
STARTTERM, ALL, BASIC and VAR.
int are non-empty sequences of digits
Examples
Example for AST with numbers
(GOAL AST)
(VAR x)
(RULES
g(x) -> 1 : g(g(x)) || 1 : x
)
Example for AST with probabilities
(GOAL AST)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)
Example for iAST
(GOAL AST)
(STRATEGY INNERMOST)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)
Example for AST considering only basic start terms
(GOAL AST)
(STARTTERM BASIC)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)
Example for certain termination
(GOAL TERMINATION)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)
Example for innermost certain termination
(GOAL TERMINATION)
(STRATEGY INNERMOST)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)
Example for innermost PAST
(GOAL PAST)
(STRATEGY INNERMOST)
(VAR x)
(RULES
g(x) -> 1/2 : g(g(x)) || 1/2 : x
)