Formula for veryfing that a state can be reached from another state?

[DavidC0rtes]

Hi, i am still new to TCTL and the way UPPPAL's verifier (verifyta) works, but

I want to ask if there's a way to specify in a formula accepted by the verifier that a certain location (B) can be reached from another one? (A). But in this case, A is not necessarily the initial location?

I've tried some with relative success:

• A simple reachability formula like E<> Process.B, but it doesn't take into account the "source" location A, if A is not the initial location.
• leads to : A --> B, but this only works if going to B from A is the only possible action.
• A SMC query like Pr[<=1;10] ((Process.A)U(Process.B)) which works but it doesn't generate an example trace (i really need an example trace).

Would like some pointers on this matter

[thorulf4]

Because Uppaal does not support nested quantifiers e.g. (A[], A<>, E[], E<>) in one query achieving your goal may require changes to your model.

I recommend adding a boolean that is set to true on edges going into location A, lets call this boolean reachedA.
Now we can check reachability using E<> reachedA && Process.B this should also provide a trace