(old) leads-to bug

(1 post) (1 voice)
  • Started 3 months ago by CharpoV
  • 1 Members Subscribed To Topic

Tags

  1. CharpoV
    Member

    I'm seing (again) a counterexample for a property of the form p ~> q in which the cycle of states is such that p is always false. This is a longstanding bug (I can provide the module if needed).

    In my desperation, I tried to use the toolbox instead of the command-line tools (although it looks both use TLC2 Version 2.03 of 20 July 2011). What I get then is "java.io.EOFException".

    Also, is setting Java's class path to toolbox/plugins/org.lamport.tlatools_1.0.0.201109181126 equivalent to using the command-line tools?

    MC

    Posted 3 months ago #

RSS feed for this topic

Reply

You must log in to post.