MC INV DLK LTL Add Job

      Start new model checking job

      Select events from the list for (inductive) invariant checking. By default, all events will be selected.

        ProB will search for a deadlocking state satisfying the invariant. You can (optionally) specify a predicate to constrain the search:

        ProB will check the following LTL Formula (CANNOT be empty):