Commit 8cfcf9b0 authored by Nam Cao's avatar Nam Cao Committed by Steven Rostedt (Google)
Browse files

verification/rvgen: Support the 'next' operator 

The 'next' operator is a unary operator. It is defined as: "next time, the
operand must be true".

Support this operator. For RV monitors, "next time" means the next
invocation of ltl_validate().

Cc: John Ogness <john.ogness@linutronix.de>
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de


Signed-off-by: default avatarNam Cao <namcao@linutronix.de>
Tested-by: default avatarGabriele Monaco <gmonaco@redhat.com>
Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
parent e93648e8

Documentation/trace/rv/linear_temporal_logic.rst

+1 −0
Original line number Diff line number Diff line
@@ -41,6 +41,7 @@ Operands (opd): 
Unary Operators (unop):

    always

    eventually

    next

    not



Binary Operators (binop):

tools/verification/rvgen/rvgen/ltl2ba.py

+26 −0
Original line number Diff line number Diff line
@@ -19,6 +19,7 @@ from ply.yacc import yacc 
# Unary Operators (unop):

#       always

#       eventually

#       next

#       not

#

# Binary Operators (binop):
@@ -35,6 +36,7 @@ tokens = ( 
   'UNTIL',

   'ALWAYS',

   'EVENTUALLY',

   'NEXT',

   'VARIABLE',

   'LITERAL',

   'NOT',
@@ -48,6 +50,7 @@ t_OR = r'or' 
t_IMPLY = r'imply'

t_UNTIL = r'until'

t_ALWAYS = r'always'

t_NEXT = r'next'

t_EVENTUALLY = r'eventually'

t_VARIABLE = r'[A-Z_0-9]+'

t_LITERAL = r'true|false'
@@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp): 
        # ![]F == <>(!F)

        return EventuallyOp(self.child.negate()).normalize()



class NextOp(UnaryOp):

    def normalize(self):

        return self



    def _is_temporal(self):

        return True



    def negate(self):

        # not (next A) == next (not A)

        self.child = self.child.negate()

        return self



    @staticmethod

    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:

        tmp = GraphNode(node.incoming,

                        node.new,

                        node.old | {n},

                        node.next | {n.op.child})

        return tmp.expand(node_set)



class NotOp(UnaryOp):

    def __str__(self):

        return "!" + str(self.child)
@@ -452,12 +475,15 @@ def p_unop(p): 
    '''

    unop : ALWAYS ltl

         | EVENTUALLY ltl

         | NEXT ltl

         | NOT ltl

    '''

    if p[1] == "always":

        op = AlwaysOp(p[2])

    elif p[1] == "eventually":

        op = EventuallyOp(p[2])

    elif p[1] == "next":

        op = NextOp(p[2])

    elif p[1] == "not":

        op = NotOp(p[2])

    else: