Errors when running new liveness tactics

[Lotan-Raz]

I installed the current version of ivy, and tried running the following files (through command line), and getting the following errors:
PS E:\Research\Programs\ivy\doc\examples\liveness> ivy_check ticket_mc.ivy
ticket_mc.ivy(168): error: token 'L': syntax error
PS E:\Research\Programs\ivy\doc\examples\liveness> ivy_check 1queuelive.ivy
1queuelive.ivy(73): error: token 'definition': syntax error

I will note that I am running ivy on windows, and I saw there is some remark that model checking is not available on windows. Is this related?

[glycerine]

If you installed a binary, you probably got IVy version 1.7, and that ticket_mc.ivy file is later:

#lang ivy1.8

so try building from source?

ivy_check ticket_mc.ivy runs for me on my mac with version 1.8.25 built from source. (takes a few minutes)...

jaten@Js-MacBook-Pro ~/pyivy/ivy/doc/examples/liveness (master) $ ivy_check ticket_mc.ivy

Isolate index.iso:

    The following definitions are used:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 54: index.impl.def14

    The following properties are to be checked:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 33: index.spec.prop4 ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 4: index.spec.transitivity ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 5: index.spec.antisymmetry ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 6: index.spec.totality ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 11: index.spec.prop1 ... PASS

Isolate this:

    The following definitions are used:
        ticket_mc.ivy: line 43: scheduled.def79
        ticket_mc.ivy: line 72: def83

    The following properties are to be checked:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 33: index.spec.prop4  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 4: index.spec.transitivity  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 5: index.spec.antisymmetry  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 6: index.spec.totality  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 11: index.spec.prop1  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 33: ticket.spec.prop4  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 4: ticket.spec.transitivity  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 5: ticket.spec.antisymmetry  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 6: ticket.spec.totality  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 11: ticket.spec.prop1  [assumed]

    The inductive invariant consists of the following conjectures:
        ticket_mc.ivy: line 50: scheduled.invar82
        ticket_mc.ivy: line 137: invar97
        ticket_mc.ivy: line 138: invar98
        ticket_mc.ivy: line 139: invar99
        ticket_mc.ivy: line 140: invar100
        ticket_mc.ivy: line 141: invar101
        ticket_mc.ivy: line 144: invar102
        ticket_mc.ivy: line 147: invar103
        ticket_mc.ivy: line 148: invar104
        ticket_mc.ivy: line 149: invar105
        ticket_mc.ivy: line 150: invar106
        ticket_mc.ivy: line 151: invar107
        ticket_mc.ivy: line 152: invar108
        ticket_mc.ivy: line 153: invar109
        ticket_mc.ivy: line 154: invar110

    The following action implementations are present:
        ticket_mc.ivy: line 38: implementation of scheduled.raise
        ticket_mc.ivy: line 65: implementation of step12
        ticket_mc.ivy: line 66: implementation of step22
        ticket_mc.ivy: line 67: implementation of step23
        ticket_mc.ivy: line 68: implementation of step31

    The following action monitors are present:
        ticket_mc.ivy: line 45: monitor of scheduled.raise
        ticket_mc.ivy: line 93: monitor of step12
        ticket_mc.ivy: line 104: monitor of step22
        ticket_mc.ivy: line 112: monitor of step23
        ticket_mc.ivy: line 121: monitor of step31
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 37: monitor of ticket.next

    The following initializers are present:
        ticket_mc.ivy: line 82: init[after84]
        ticket_mc.ivy: line 44: scheduled.init[after80]

    Initialization must establish the invariant
        ticket_mc.ivy: line 50: scheduled.invar82 ... PASS
        ticket_mc.ivy: line 137: invar97 ... PASS
        ticket_mc.ivy: line 138: invar98 ... PASS
        ticket_mc.ivy: line 139: invar99 ... PASS
        ticket_mc.ivy: line 140: invar100 ... PASS
        ticket_mc.ivy: line 141: invar101 ... PASS
        ticket_mc.ivy: line 144: invar102 ... PASS
        ticket_mc.ivy: line 147: invar103 ... PASS
        ticket_mc.ivy: line 148: invar104 ... PASS
        ticket_mc.ivy: line 149: invar105 ... PASS
        ticket_mc.ivy: line 150: invar106 ... PASS
        ticket_mc.ivy: line 151: invar107 ... PASS
        ticket_mc.ivy: line 152: invar108 ... PASS
        ticket_mc.ivy: line 153: invar109 ... PASS
        ticket_mc.ivy: line 154: invar110 ... PASS

    The following set of external actions must preserve the invariant:
        (internal) ext:step12
            ticket_mc.ivy: line 50: scheduled.invar82 ... PASS
            ticket_mc.ivy: line 137: invar97 ... PASS
            ticket_mc.ivy: line 138: invar98 ... PASS
            ticket_mc.ivy: line 139: invar99 ... PASS
            ticket_mc.ivy: line 140: invar100 ... PASS
            ticket_mc.ivy: line 141: invar101 ... PASS
            ticket_mc.ivy: line 144: invar102 ... PASS
            ticket_mc.ivy: line 147: invar103 ... PASS
            ticket_mc.ivy: line 148: invar104 ... PASS
            ticket_mc.ivy: line 149: invar105 ... PASS
            ticket_mc.ivy: line 150: invar106 ... PASS
            ticket_mc.ivy: line 151: invar107 ... PASS
            ticket_mc.ivy: line 152: invar108 ... PASS
            ticket_mc.ivy: line 153: invar109 ... PASS
            ticket_mc.ivy: line 154: invar110 ... PASS
        (internal) ext:step22
            ticket_mc.ivy: line 50: scheduled.invar82 ... PASS
            ticket_mc.ivy: line 137: invar97 ... PASS
            ticket_mc.ivy: line 138: invar98 ... PASS
            ticket_mc.ivy: line 139: invar99 ... PASS
            ticket_mc.ivy: line 140: invar100 ... PASS
            ticket_mc.ivy: line 141: invar101 ... PASS
            ticket_mc.ivy: line 144: invar102 ... PASS
            ticket_mc.ivy: line 147: invar103 ... PASS
            ticket_mc.ivy: line 148: invar104 ... PASS
            ticket_mc.ivy: line 149: invar105 ... PASS
            ticket_mc.ivy: line 150: invar106 ... PASS
            ticket_mc.ivy: line 151: invar107 ... PASS
            ticket_mc.ivy: line 152: invar108 ... PASS
            ticket_mc.ivy: line 153: invar109 ... PASS
            ticket_mc.ivy: line 154: invar110 ... PASS
        (internal) ext:step23
            ticket_mc.ivy: line 50: scheduled.invar82 ... PASS
            ticket_mc.ivy: line 137: invar97 ... PASS
            ticket_mc.ivy: line 138: invar98 ... PASS
            ticket_mc.ivy: line 139: invar99 ... PASS
            ticket_mc.ivy: line 140: invar100 ... PASS
            ticket_mc.ivy: line 141: invar101 ... PASS
            ticket_mc.ivy: line 144: invar102 ... PASS
            ticket_mc.ivy: line 147: invar103 ... PASS
            ticket_mc.ivy: line 148: invar104 ... PASS
            ticket_mc.ivy: line 149: invar105 ... PASS
            ticket_mc.ivy: line 150: invar106 ... PASS
            ticket_mc.ivy: line 151: invar107 ... PASS
            ticket_mc.ivy: line 152: invar108 ... PASS
            ticket_mc.ivy: line 153: invar109 ... PASS
            ticket_mc.ivy: line 154: invar110 ... PASS
        (internal) ext:step31
            ticket_mc.ivy: line 50: scheduled.invar82 ... PASS
            ticket_mc.ivy: line 137: invar97 ... PASS
            ticket_mc.ivy: line 138: invar98 ... PASS
            ticket_mc.ivy: line 139: invar99 ... PASS
            ticket_mc.ivy: line 140: invar100 ... PASS
            ticket_mc.ivy: line 141: invar101 ... PASS
            ticket_mc.ivy: line 144: invar102 ... PASS
            ticket_mc.ivy: line 147: invar103 ... PASS
            ticket_mc.ivy: line 148: invar104 ... PASS
            ticket_mc.ivy: line 149: invar105 ... PASS
            ticket_mc.ivy: line 150: invar106 ... PASS
            ticket_mc.ivy: line 151: invar107 ... PASS
            ticket_mc.ivy: line 152: invar108 ... PASS
            ticket_mc.ivy: line 153: invar109 ... PASS
            ticket_mc.ivy: line 154: invar110 ... PASS

    The following program assertions are treated as assumptions:
        in action ticket.next when called from step12,step31:
            /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 38: assumption
            /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 39: assumption
        in action step12 when called from the environment:
            ticket_mc.ivy: line 94: assumption
        in action step22 when called from the environment:
            ticket_mc.ivy: line 105: assumption
            ticket_mc.ivy: line 106: assumption
            ticket_mc.ivy: line 107: assumption
        in action step23 when called from the environment:
            ticket_mc.ivy: line 113: assumption
            ticket_mc.ivy: line 114: assumption
            ticket_mc.ivy: line 115: assumption
        in action step31 when called from the environment:
            ticket_mc.ivy: line 122: assumption

    The following temporal property is being proved:

        ticket_mc.ivy: line 164: lemma1 ... PASS


    The following temporal property is being proved:

        ticket_mc.ivy: line 171: live ... PASS


Isolate ticket.iso:

    The following definitions are used:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 54: ticket.impl.def14

    The following properties are to be checked:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 33: index.spec.prop4  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 4: index.spec.transitivity  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 5: index.spec.antisymmetry  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 6: index.spec.totality  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 11: index.spec.prop1  [assumed]
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 33: ticket.spec.prop4 ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 4: ticket.spec.transitivity ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 5: ticket.spec.antisymmetry ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 6: ticket.spec.totality ... PASS
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 11: ticket.spec.prop1 ... PASS

    The following action implementations are present:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 57: implementation of ticket.next

    The following action monitors are present:
        /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 37: monitor of ticket.next

    The following program assertions are treated as guarantees:
        in action ticket.next when called from the environment:
            /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 38: guarantee ... PASS
            /Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/include/1.8/order.ivy: line 39: guarantee ... PASS

OK
jaten@Js-MacBook-Pro ~/pyivy/ivy/doc/examples/liveness (master) $