关于Uppaal火车闸机示例代码报错的求助及完整代码需求

问题描述 #

严格使用Uppaal官方及网络上的火车闸机示例代码时，出现语法错误与未定义错误，尝试相关示例代码后仍无法解决，急需完整可运行的示例代码。当前使用的代码片段如下：

【项目声明】
const int N = 6;
typedeft int [0,N-1] id_t;
chan appr,stop,go,leave;
urgent chan go;
【闸机声明】
id_t list [N+1];
int[0,N] len;

void enqueue(id_t element)
{
    list[len++] = element;
}

void dequeue()
{
    int i = 0;
    len -=1;
    while(i < len)
    {
        list[i] = list[i+1];
        i++;
    }
    list[i]=0;
}
id_t front()
{
return list [0];
}

id_t tail () 
{
return list [ len − 1];
}
【火车声明】
clock x;
【系统声明】
Process = Template();
Train1:=Train(e1,1);
Train2:=Train(e1,2);
Train3:=Train(e1,3);
Train4:=Train(e1,4);

system Process;
Train1,Train2,Train3,Train4,Gate,Queue

错误修正及完整可运行代码 #

全局声明部分（项目+闸机通用声明） #

const int N = 6;
typedef int[0,N-1] id_t; // 修正typedeft拼写错误
chan appr, stop, go, leave;
urgent chan go;

// 闸机队列声明
id_t list[N+1];
int[0,N] len = 0; // 初始化长度，避免未定义值

void enqueue(id_t element)
{
    list[len++] = element;
}

void dequeue()
{
    int i = 0;
    len -= 1;
    while(i < len)
    {
        list[i] = list[i+1];
        i++;
    }
    list[i] = 0;
}

id_t front()
{
    return list[0]; // 修正空格语法问题
}

id_t tail() 
{
    return list[len - 1]; // 修正全角减号为半角
}

火车模板（命名为Train） #

需创建对应状态：Idle（初始状态）、Approaching、Waiting、Crossing、Leaving，代码如下：

template Train(id_t id)
{
    clock x;
    // 状态定义
    location Idle: initial;
    location Approaching;
    location Waiting;
    location Crossing;
    location Leaving;

    // 迁移逻辑
    edge Idle -> Approaching {
        sync: appr!id;
        assignment: x = 0;
    }

    edge Approaching -> Waiting {
        guard: x >= 2;
        sync: stop?id;
    }

    edge Waiting -> Crossing {
        sync: go?id;
        assignment: x = 0;
    }

    edge Crossing -> Leaving {
        guard: x >= 3;
        sync: leave!id;
    }

    edge Leaving -> Idle;
}

闸机模板（命名为Gate） #

需创建对应状态：Closed（初始状态）、Open，代码如下：

template Gate()
{
    location Closed: initial;
    location Open;

    // 迁移逻辑
    edge Closed -> Open {
        guard: len > 0;
        sync: go!front();
    }

    edge Open -> Closed {
        sync: leave?[front()];
        assignment: dequeue();
    }
}

队列处理模板（命名为Queue） #

需创建对应状态：Running（初始状态），代码如下：

template Queue()
{
    location Running: initial;

    // 迁移逻辑
    edge Running -> Running {
        sync: appr?id;
        assignment: enqueue(id);
        sync: stop!id;
    }
}

系统声明部分 #

// 实例化组件
Train1 := Train(1);
Train2 := Train(2);
Train3 := Train(3);
Train4 := Train(4);
Gate1 := Gate();
Queue1 := Queue();

// 定义系统
system Train1, Train2, Train3, Train4, Gate1, Queue1;

使用说明 #

1. 将上述代码按对应部分粘贴到Uppaal编辑器中
2. 确保每个模板匹配对应的可视化状态图（或直接使用代码模式导入）
3. 检查无语法错误后，即可进行模型验证

内容的提问来源于stack exchange，提问作者nazlı özdemir