Add PRISM backend to probably

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)

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
+"""

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, program)};\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.lower})..({typ.bounds.upper})];\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 : [0..{len(graph)}] 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, program)
+    prism_program += "endmodule\n"
+    return prism_program

probably/prism/translate.py

@@ -0,0 +1,187 @@
+"""
+--------------------
+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, 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
+    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, program: Program):
+        return f"({var}'={expression_prism(value, program)})"
+
+    assignment_string = " + ".join([
+        (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"
+
+    # 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, 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, 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")
+
+    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 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], 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.
+    """
+    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, program)
+        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, program)
+        rhs = expression_prism(expr.rhs, program)
+        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.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:
+            return f"({lhs}) + ({rhs})"
+        elif expr.operator == Binop.MINUS:
+            return f"({lhs}) - ({rhs})"
+        elif expr.operator == Binop.TIMES:
+            return f"({lhs}) * ({rhs})"
+        elif expr.operator == Binop.MODULO:
+            return f"mod({lhs}, {rhs})"
+        elif expr.operator == Binop.POWER:
+            return f"pow({lhs}, {rhs})"
+        elif expr.operator == Binop.DIVIDE:
+            # 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(
+            "Substitution expression not implemented:", expr)
+    raise PrismTranslatorException("Operator not implemented:", expr)

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)