[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] small bug in TLC gui

   On the TLC model overview page:
  1. You can instantiate the parameters (CONSTANTS)  initially the screen is white text on grey background but when you change the type  (Model value -> Ordinary assignment, .... or what ever) the screen is the unhelpful white text on white background.
  2. Not sure if this is a bug or restriction we need to work with:
       From ABSpec "Inv == AVar[2]= BVar[2] => (AVar = Bvar)"  but Inv is not recognised as an Invariant whereas the right hand side is.
       I previously noticed that in a definition I could not use any previous definitions.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ff6d3a2b-e848-4783-8c88-58866f4a18f2%40googlegroups.com.