From c65b76237e0a87008c5ceb61355d5aeef7e57636 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 20:35:17 +0200 Subject: [PATCH 1/6] Add PRISM backend to probably --- probably/cmd.py | 15 +++- probably/prism/__init__.py | 12 +++ probably/prism/backend.py | 64 ++++++++++++++++ probably/prism/translate.py | 148 ++++++++++++++++++++++++++++++++++++ tests/test_prism.py | 55 ++++++++++++++ 5 files changed, 290 insertions(+), 4 deletions(-) create mode 100644 probably/prism/__init__.py create mode 100644 probably/prism/backend.py create mode 100644 probably/prism/translate.py create mode 100644 tests/test_prism.py diff --git a/probably/cmd.py b/probably/cmd.py index 8f6eaa6..a45685f 100644 --- a/probably/cmd.py +++ b/probably/cmd.py @@ -19,24 +19,31 @@ from probably.pgcl.check import CheckFail from probably.pgcl.syntax import check_is_linear_program from probably.pgcl.wp import general_wp_transformer +from probably.prism.backend import translate_to_prism @click.command() -@click.argument('input', type=click.File('r')) +@click.argument("input", type=click.File('r')) +@click.option("--prism", is_flag=True, default=False) # pylint: disable=redefined-builtin -def main(input: IO): +def main(input: IO, prism: bool): """ Compile the given program and print some information about it. """ program_source = input.read() - print("Program source:") - print(program_source) program = pgcl.compile_pgcl(program_source) if isinstance(program, CheckFail): print("Error:", program) return + if prism: + print(translate_to_prism(program)) + return + + print("Program source:") + print(program_source) + print("Program instructions:") for instr in program.instructions: pprint.pprint(instr) diff --git a/probably/prism/__init__.py b/probably/prism/__init__.py new file mode 100644 index 0000000..15ff042 --- /dev/null +++ b/probably/prism/__init__.py @@ -0,0 +1,12 @@ +""" +================== +``probably.prism`` +================== + +Probably contains some utility functions to translate parts of a pGCL program to +PRISM. + + +.. automodule:: probably.pysmt.backend +.. automodule:: probably.pysmt.translate +""" diff --git a/probably/prism/backend.py b/probably/prism/backend.py new file mode 100644 index 0000000..86da377 --- /dev/null +++ b/probably/prism/backend.py @@ -0,0 +1,64 @@ +""" +----------------- +The PRISM Backend +----------------- + +This module can translate pCGL Programs to PRISM Programs with the function +translate_to_prism. +""" + +from probably.pgcl.ast.program import Program +from probably.pgcl.ast.types import NatType +from probably.pgcl.cfg import ControlFlowGraph +from probably.prism.translate import (PrismTranslatorException, block_prism, + expression_prism, type_prism) + + +def translate_to_prism(program: Program) -> str: + """ + Translate a pCGL program to a PRISM program. The PRISM program shares the + same variable names as the pCGL programs, so you can ask a model checker + like Storm for conditions on these variables: + + What is the probability that the boolean done is, at some point, true? + P=? [F (done)] + + What is the probability that the natural number c is always zero? + P=? [G c=0] + + The PRISM program has a single module named "program". The input program + may not use the variable names "ppc" and "ter". + """ + # Initialize variables + prism_program = "dtmc\n" + # pCGL constants are interpreted as PRISM constants + for (var, value) in program.constants.items(): + prism_program += f"const {var} = {expression_prism(value)};\n" + prism_program += "module program\n" + # Parameters and variables are PRISM variables + for (var, typ) in list(program.parameters.items()) + list( + program.variables.items()): + if isinstance(typ, NatType) and typ.bounds is not None: + prism_program += f"{var} : {typ.bounds};\n" + else: + prism_program += f"{var} : {type_prism(typ)};\n" + + graph = ControlFlowGraph.from_instructions(program.instructions) + + # Initialize prism's program counter ppc + if "ppc" in [x.var for x in program.declarations]: + raise PrismTranslatorException( + "Don't declare a variable called ppc, that's needed by the PRISM translator." + ) + prism_program += f"ppc : int init {graph.entry_id};\n" + # Initialize terminator execution bool + if "ppc" in [x.var for x in program.declarations]: + raise PrismTranslatorException( + "Don't declare a variable called ter, that's needed by the PRISM translator." + ) + prism_program += "ter : bool init false;\n" + + for block in graph: + prism_program += block_prism(block) + prism_program += "endmodule\n" + return prism_program diff --git a/probably/prism/translate.py b/probably/prism/translate.py new file mode 100644 index 0000000..598b1d8 --- /dev/null +++ b/probably/prism/translate.py @@ -0,0 +1,148 @@ +""" +-------------------- +The PRISM Translator +-------------------- + +Internal functions for translating parts of a pCGL control graph / program to +PRISM snippets, used by probably.prism.backend. +""" + +from typing import Any + +from probably.pgcl.ast import * +from probably.pgcl.cfg import BasicBlock, TerminatorKind + + +class PrismTranslatorException(Exception): + pass + + +def block_prism(block: BasicBlock) -> str: + """ + Translate a pGCL block to a PRISM snippet. There are multiple state + transitions for each block, at least one for the program part and one for + the terminator. + """ + prism_program = "" + # from probabilities to assignments + # with probability 1: go to terminator + distribution: Any = [(1.0, [("ter", BoolLitExpr(True))])] + + for assignment in block.assignments: + var = assignment[0] + expr = assignment[1] + # prism does the distributions in a different order, just globally + # outside the assignments. that's why we explicitely have to list + # all cases. + if isinstance(expr, CategoricalExpr): + new_distribution = [] + for prob_old, other_assignments in distribution: + for prob_new, value in expr.distribution(): + new_distribution.append( + (prob_old * prob_new.to_fraction(), + other_assignments + [(var, value)])) + distribution = new_distribution + else: + for _, other_assignments in distribution: + other_assignments.append((var, expr)) + condition = f"ter=false & ppc={block.ident}" + + def make_expression(var: Var, value: Expr): + return f"({var}'={expression_prism(value)})" + + assignment_string = " + ".join([ + (f"{prob} : " if prob < 1 else "") + + "&".join([make_expression(var, value) for var, value in assignments]) + for prob, assignments in distribution + ]) + block_logic = f"[] ({condition}) -> {assignment_string};\n" + + # if these gotos are None, this means quit the program, which we translate + # as ppc == -1 + if block.terminator.if_true is None: + goto_true = -1 + else: + goto_true = block.terminator.if_true + + if block.terminator.if_false is None: + goto_false = -1 + else: + goto_false = block.terminator.if_false + + if block.terminator.is_goto(): + terminator_logic = f"[] (ter=true & ppc={block.ident}) -> (ter'=false)&(ppc'={goto_true});\n" + elif block.terminator.kind == TerminatorKind.BOOLEAN: + cond = expression_prism(block.terminator.condition) + terminator_logic = "".join([ + f"[] (ter=true & ppc={block.ident} & {cond}) -> (ter'=false)&(ppc'={goto_true});\n" + f"[] (ter=true & ppc={block.ident} & !({cond})) -> (ter'=false)&(ppc'={goto_false});\n" + ]) + elif block.terminator.kind == TerminatorKind.PROBABILISTIC: + cond = expression_prism(block.terminator.condition) + terminator_logic = f"[] (ter=true & ppc={block.ident}) -> {cond} : (ppc'={goto_true})&(ter'=false) + 1-({cond}) : (ppc'={goto_false})&(ter'=false);\n" + else: + raise RuntimeError(f"{block.terminator} not implemented") + + prism_program = block_logic + terminator_logic + return prism_program + + +def type_prism(typ: Type) -> str: + """ + Translate a pGCL type to a PRISM type. + """ + if isinstance(typ, BoolType): + return "bool" + elif isinstance(typ, NatType): + return "int" + elif isinstance(typ, RealType): + return "double" + raise PrismTranslatorException("Type not implemented:", typ) + + +def expression_prism(expr: Expr) -> str: + """ + Translate a pGCL expression to a PRISM expression. + """ + if isinstance(expr, BoolLitExpr): + return "true" if expr.value else "false" + elif isinstance(expr, NatLitExpr): + # PRISM understands natural numbers + return str(expr.value) + elif isinstance(expr, RealLitExpr): + # PRISM understands fractions + return str(expr.to_fraction()) + elif isinstance(expr, VarExpr): + # Var == str + return str(expr.var) + elif isinstance(expr, UnopExpr): + operand = expression_prism(expr.expr) + if expr.operator == Unop.NEG: + return f"!({operand})" + elif expr.operator == Unop.IVERSON: + raise PrismTranslatorException( + "Not implemented: iverson brackets like", expr) + raise PrismTranslatorException("Operator not implemented:", expr) + elif isinstance(expr, BinopExpr): + lhs = expression_prism(expr.lhs) + rhs = expression_prism(expr.rhs) + if expr.operator == Binop.OR: + return f"({lhs}) | ({rhs})" + elif expr.operator == Binop.AND: + return f"({lhs}) & ({rhs})" + elif expr.operator == Binop.LEQ: + return f"({lhs}) <= ({rhs})" + elif expr.operator == Binop.LT: + return f"({lhs}) < ({rhs})" + elif expr.operator == Binop.EQ: + return f"({lhs}) = ({rhs})" + elif expr.operator == Binop.PLUS: + return f"({lhs}) + ({rhs})" + elif expr.operator == Binop.MINUS: + return f"({lhs}) - ({rhs})" + elif expr.operator == Binop.TIMES: + return f"({lhs}) * ({rhs})" + elif isinstance(expr, SubstExpr): + raise PrismTranslatorException( + "Substitution expression not implemented:", expr) + raise PrismTranslatorException("Operator not implemented:", expr) diff --git a/tests/test_prism.py b/tests/test_prism.py new file mode 100644 index 0000000..101c4ff --- /dev/null +++ b/tests/test_prism.py @@ -0,0 +1,55 @@ +from probably.pgcl.compiler import parse_pgcl +from probably.prism.backend import translate_to_prism + + +def test_ber_ert(): + program = parse_pgcl(""" + nat x; + nat n; + nat r; + while (x < n) { + r := 1 : 1/2 + 0 : 1/2; + x := x + r; + tick(1); + } + """) + translate_to_prism(program) + + +def test_linear01(): + program = parse_pgcl(""" + nat x; + while (2 <= x) { + { x := x - 1; } [1/3] { + x := x - 2; + } + tick(1); + } + """) + translate_to_prism(program) + + +def test_prspeed(): + program = parse_pgcl(""" + nat x; + nat y; + nat m; + nat n; + while ((x + 3 <= n)) { + if (y < m) { + { y := y + 1; } [1/2] { + y := y + 0; + } + } else { + { x := x + 0; } [1/4] { + { x := x + 1; } [1/3] { + { x := x + 2; } [1/2] { + x := x + 3; + } + } + } + } + tick(1); + } + """) + translate_to_prism(program) From c6eb165d88f841d2ce4d6601ca1b20138b043042 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 20:58:32 +0200 Subject: [PATCH 2/6] Add Binops --- probably/prism/translate.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/probably/prism/translate.py b/probably/prism/translate.py index 598b1d8..05b4f6c 100644 --- a/probably/prism/translate.py +++ b/probably/prism/translate.py @@ -134,6 +134,10 @@ def expression_prism(expr: Expr) -> str: return f"({lhs}) <= ({rhs})" elif expr.operator == Binop.LT: return f"({lhs}) < ({rhs})" + elif expr.operator == Binop.GEQ: + return f"({lhs}) <= ({rhs})" + elif expr.operator == Binop.GT: + return f"({lhs}) < ({rhs})" elif expr.operator == Binop.EQ: return f"({lhs}) = ({rhs})" elif expr.operator == Binop.PLUS: @@ -142,6 +146,9 @@ def expression_prism(expr: Expr) -> str: return f"({lhs}) - ({rhs})" elif expr.operator == Binop.TIMES: return f"({lhs}) * ({rhs})" + elif expr.operator == Binop.MODULO: + return f"({lhs}) * ({rhs})" + raise PrismTranslatorException("Operator not implemented:", expr) elif isinstance(expr, SubstExpr): raise PrismTranslatorException( "Substitution expression not implemented:", expr) From 9b29231a914f7326ea06a9b55940a5fd4850154f Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 21:07:50 +0200 Subject: [PATCH 3/6] Fix modulo, add power and divide --- probably/prism/translate.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/probably/prism/translate.py b/probably/prism/translate.py index 05b4f6c..9b002f5 100644 --- a/probably/prism/translate.py +++ b/probably/prism/translate.py @@ -147,7 +147,11 @@ def expression_prism(expr: Expr) -> str: elif expr.operator == Binop.TIMES: return f"({lhs}) * ({rhs})" elif expr.operator == Binop.MODULO: - return f"({lhs}) * ({rhs})" + return f"mod({lhs}, {rhs})" + elif expr.operator == Binop.POWER: + return f"pow({lhs}, {rhs})" + elif expr.operator == Binop.DIVIDE: + return f"{lhs} / {rhs}" raise PrismTranslatorException("Operator not implemented:", expr) elif isinstance(expr, SubstExpr): raise PrismTranslatorException( From c167620a711de65b9ed1c54cd2392938487ee816 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 22:43:57 +0200 Subject: [PATCH 4/6] Fix: floor() for integer divisions --- probably/prism/backend.py | 4 +-- probably/prism/translate.py | 54 ++++++++++++++++++++++++++++--------- 2 files changed, 43 insertions(+), 15 deletions(-) diff --git a/probably/prism/backend.py b/probably/prism/backend.py index 86da377..137a974 100644 --- a/probably/prism/backend.py +++ b/probably/prism/backend.py @@ -33,7 +33,7 @@ def translate_to_prism(program: Program) -> str: prism_program = "dtmc\n" # pCGL constants are interpreted as PRISM constants for (var, value) in program.constants.items(): - prism_program += f"const {var} = {expression_prism(value)};\n" + prism_program += f"const {var} = {expression_prism(value, program)};\n" prism_program += "module program\n" # Parameters and variables are PRISM variables for (var, typ) in list(program.parameters.items()) + list( @@ -59,6 +59,6 @@ def translate_to_prism(program: Program) -> str: prism_program += "ter : bool init false;\n" for block in graph: - prism_program += block_prism(block) + prism_program += block_prism(block, program) prism_program += "endmodule\n" return prism_program diff --git a/probably/prism/translate.py b/probably/prism/translate.py index 9b002f5..9f1ac1f 100644 --- a/probably/prism/translate.py +++ b/probably/prism/translate.py @@ -17,7 +17,7 @@ class PrismTranslatorException(Exception): pass -def block_prism(block: BasicBlock) -> str: +def block_prism(block: BasicBlock, program: Program) -> str: """ Translate a pGCL block to a PRISM snippet. There are multiple state transitions for each block, at least one for the program part and one for @@ -47,13 +47,13 @@ def block_prism(block: BasicBlock) -> str: other_assignments.append((var, expr)) condition = f"ter=false & ppc={block.ident}" - def make_expression(var: Var, value: Expr): - return f"({var}'={expression_prism(value)})" + def make_expression(var: Var, value: Expr, program: Program): + return f"({var}'={expression_prism(value, program)})" assignment_string = " + ".join([ - (f"{prob} : " if prob < 1 else "") + - "&".join([make_expression(var, value) for var, value in assignments]) - for prob, assignments in distribution + (f"{prob} : " if prob < 1 else "") + "&".join([ + make_expression(var, value, program) for var, value in assignments + ]) for prob, assignments in distribution ]) block_logic = f"[] ({condition}) -> {assignment_string};\n" @@ -72,13 +72,13 @@ def make_expression(var: Var, value: Expr): if block.terminator.is_goto(): terminator_logic = f"[] (ter=true & ppc={block.ident}) -> (ter'=false)&(ppc'={goto_true});\n" elif block.terminator.kind == TerminatorKind.BOOLEAN: - cond = expression_prism(block.terminator.condition) + cond = expression_prism(block.terminator.condition, program) terminator_logic = "".join([ f"[] (ter=true & ppc={block.ident} & {cond}) -> (ter'=false)&(ppc'={goto_true});\n" f"[] (ter=true & ppc={block.ident} & !({cond})) -> (ter'=false)&(ppc'={goto_false});\n" ]) elif block.terminator.kind == TerminatorKind.PROBABILISTIC: - cond = expression_prism(block.terminator.condition) + cond = expression_prism(block.terminator.condition, program) terminator_logic = f"[] (ter=true & ppc={block.ident}) -> {cond} : (ppc'={goto_true})&(ter'=false) + 1-({cond}) : (ppc'={goto_false})&(ter'=false);\n" else: raise RuntimeError(f"{block.terminator} not implemented") @@ -100,7 +100,30 @@ def type_prism(typ: Type) -> str: raise PrismTranslatorException("Type not implemented:", typ) -def expression_prism(expr: Expr) -> str: +def is_int(expr: Expr, program: Program): + """ + Whether an expression is at its core an integer (natural number). + """ + if isinstance(expr, NatLitExpr): + return True + if isinstance(expr, VarExpr): + if expr.var in program.variables and isinstance( + program.variables[expr.var], NatType): + return True + if expr.var in program.parameters and isinstance( + program.parameters[expr.var], NatType): + return True + if expr.var in program.constants and isinstance( + program.constants[expr.var].value, NatLitExpr): + return True + if isinstance(expr, UnopExpr): + return is_int(expr.expr, program) + if isinstance(expr, BinopExpr): + return is_int(expr.lhs, program) and is_int(expr.rhs, program) + return False + + +def expression_prism(expr: Expr, program: Program) -> str: """ Translate a pGCL expression to a PRISM expression. """ @@ -116,7 +139,7 @@ def expression_prism(expr: Expr) -> str: # Var == str return str(expr.var) elif isinstance(expr, UnopExpr): - operand = expression_prism(expr.expr) + operand = expression_prism(expr.expr, program) if expr.operator == Unop.NEG: return f"!({operand})" elif expr.operator == Unop.IVERSON: @@ -124,8 +147,8 @@ def expression_prism(expr: Expr) -> str: "Not implemented: iverson brackets like", expr) raise PrismTranslatorException("Operator not implemented:", expr) elif isinstance(expr, BinopExpr): - lhs = expression_prism(expr.lhs) - rhs = expression_prism(expr.rhs) + lhs = expression_prism(expr.lhs, program) + rhs = expression_prism(expr.rhs, program) if expr.operator == Binop.OR: return f"({lhs}) | ({rhs})" elif expr.operator == Binop.AND: @@ -151,7 +174,12 @@ def expression_prism(expr: Expr) -> str: elif expr.operator == Binop.POWER: return f"pow({lhs}, {rhs})" elif expr.operator == Binop.DIVIDE: - return f"{lhs} / {rhs}" + # PRISM doesn't have the concept of integer division, so we need to + # cook this ourselves + if is_int(expr.lhs, program) and is_int(expr.rhs, program): + return f"floor({lhs} / {rhs})" + else: + return f"{lhs} / {rhs}" raise PrismTranslatorException("Operator not implemented:", expr) elif isinstance(expr, SubstExpr): raise PrismTranslatorException( From bfaffd82c5f78d062b109c0eb0ea0d10d453ea48 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 22:56:12 +0200 Subject: [PATCH 5/6] Fix bounds --- probably/prism/backend.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/probably/prism/backend.py b/probably/prism/backend.py index 137a974..3caed53 100644 --- a/probably/prism/backend.py +++ b/probably/prism/backend.py @@ -39,7 +39,7 @@ def translate_to_prism(program: Program) -> str: for (var, typ) in list(program.parameters.items()) + list( program.variables.items()): if isinstance(typ, NatType) and typ.bounds is not None: - prism_program += f"{var} : {typ.bounds};\n" + prism_program += f"{var} : [({typ.bounds.lower})..({typ.bounds.upper})];\n" else: prism_program += f"{var} : {type_prism(typ)};\n" @@ -50,7 +50,7 @@ def translate_to_prism(program: Program) -> str: raise PrismTranslatorException( "Don't declare a variable called ppc, that's needed by the PRISM translator." ) - prism_program += f"ppc : int init {graph.entry_id};\n" + prism_program += f"ppc : [0..{len(graph)}] init {graph.entry_id};\n" # Initialize terminator execution bool if "ppc" in [x.var for x in program.declarations]: raise PrismTranslatorException( From 785a6ba653b542b88db248564090479aef667aeb Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Sun, 24 Sep 2023 23:22:08 +0200 Subject: [PATCH 6/6] Fix mypy check --- probably/prism/translate.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/probably/prism/translate.py b/probably/prism/translate.py index 9f1ac1f..b93a1aa 100644 --- a/probably/prism/translate.py +++ b/probably/prism/translate.py @@ -114,7 +114,7 @@ def is_int(expr: Expr, program: Program): program.parameters[expr.var], NatType): return True if expr.var in program.constants and isinstance( - program.constants[expr.var].value, NatLitExpr): + program.constants[expr.var], NatLitExpr): return True if isinstance(expr, UnopExpr): return is_int(expr.expr, program)