UPPAAL Stratego进程守卫引用其他进程位置的实现与疑问

1. 冗余变量是否会增加状态空间？ #

是的，肯定会。UPPAAL的系统状态由所有非meta变量的取值、时钟值、以及每个进程的当前位置共同构成。你新增的main_current_location作为普通整数变量，它的每个不同取值都会和其他状态元素（比如var的值、clk的时钟值、各个进程的位置）组合，直接扩大状态空间的规模。比如如果main进程有5个不同位置，这个变量就有5种可能取值，状态数会对应增加5倍左右（具体倍数取决于其他状态元素的组合数量）。

2. 其他实现相同目标的方案 #

• 同步/异步通道传递位置标记：在main进程的每个位置入口添加位置通知动作，比如进入running位置时执行main_pos!('running')。可以专门做一个tracker进程接收这些信号并维护位置状态，checker进程通过查询tracker的状态获取main的位置；也可以用异步通道避免main进程等待接收方响应，防止干扰原有系统执行逻辑。
• 将检查逻辑内联到目标进程：如果checker的守卫逻辑是为了触发特定动作，可直接把逻辑移到main进程中。比如当main处于running位置，且满足var==3、clk<=5时，直接通过通道发送checker_trigger!()触发checker的对应动作。这种方式无需额外维护跟踪变量，也不会增加状态空间，前提是逻辑可拆分到目标进程中。
• 封装位置检查逻辑：利用UPPAAL的宏定义功能，把位置对应的变量判断逻辑封装成宏，比如#define MAIN_RUNNING (main_current_location==1)，这样代码更整洁，维护时只需修改宏的定义内容。

3. 请求添加跨进程位置引用功能是否合理？ #

这个需求完全合理，但需要考虑几个潜在问题：

• 验证性能影响：UPPAAL内部其实已经在状态中跟踪所有进程的位置，但语法上不允许直接引用。开放该功能后，验证引擎需要处理跨进程位置的查询逻辑，虽然不会增加状态空间（位置本来就是状态的一部分），但可能会增加守卫条件的计算开销，尤其是在大规模模型中。
• 模型可维护性风险：直接引用进程位置会让模型更直观，但如果main进程的位置名称修改，所有引用该位置的守卫都需要同步修改；而用变量编码的方式只需要修改变量赋值的地方，维护成本更低。
• 多实例语义歧义：如果系统中有多个main进程实例，main.running这种写法会产生歧义，需要明确指定实例名（比如main[0].running），这会增加语法复杂度，需要工具支持实例化进程的位置引用。

总的来说，这个功能在单实例场景下非常实用，但工具开发者需要解决多实例语义、语法解析以及验证性能的问题。

内容的提问来源于stack exchange，提问作者Renaud Pacalet