如何为MiniZinc的regular函数构建多状态转移DFA？

一、处理非确定性有限自动机（NFA）场景 #

MiniZinc的regular函数仅支持*确定性有限自动机（DFA）*的转移数组，若业务逻辑是NFA（单个状态对应同一输入存在多个转移目标），必须先将NFA转换为等价的DFA，再传入函数。

转换核心是用状态集合作为DFA的新状态：将NFA中所有可能的状态组合映射为单个整数状态，再计算每个新状态对应各输入的转移集合，最终生成符合要求的DFA转移数组。

示例：NFA转DFA #

假设NFA规则：

• 状态1，输入0→{2,3}；输入1→{1}
• 状态2，输入0→{4}；输入1→{1}
• 状态3，输入0→{4}；输入1→{5}
• 状态4，输入0/1→{6}
• 状态5，输入0→{6}；输入1→死状态（0）
• 状态6，输入0/1→死状态（0）

先映射状态集合为DFA整数状态：

• {} → 0（死状态）
• {1} →1
• {2,3} →2
• {4} →3
• {5} →4
• {6} →5

构建DFA转移数组：

set of int: STATE = 0..5;
set of int: INPUT = 0..1;
array[STATE, INPUT] of int: t = [|
    0, 0,    % 死状态：任何输入保持死状态
    2, 1,    % 状态1({1})：输入0→状态2({2,3})，输入1→状态1
    3, 4,    % 状态2({2,3})：输入0→状态3({4})，输入1→状态4({5})
    5, 5,    % 状态3({4})：输入0/1→状态5({6})
    5, 0,    % 状态4({5})：输入0→状态5，输入1→死状态
    0, 0     % 状态5({6})：任何输入→死状态
|];

二、处理非布尔型激励变量场景 #

若激励变量是多值整数（如取值0、1、2），只需将转移数组的第二维度（输入维度）对应所有可能的输入值，确保每个状态对每个输入值都有明确的转移目标即可。

示例：三值激励变量 #

假设激励变量x取值为0、1、2，状态转移规则如下：

• 状态1：输入0→2，输入1→3，输入2→1
• 状态2：输入0/1→4，输入2→1
• 状态3：输入0→4，输入1→5，输入2→1
• 状态4：输入0/1→6，输入2→1
• 状态5：输入0→6，输入1→死状态（0），输入2→1
• 状态6：输入0/1→死状态（0），输入2→1

对应的转移数组：

set of int: STATE = 0..6;
set of int: INPUT = 0..2;
array[STATE, INPUT] of int: t = [|
    0, 0, 0,    % 死状态：任何输入保持死状态
    2, 3, 1,    % 状态1
    4, 4, 1,    % 状态2
    4, 5, 1,    % 状态3
    6, 6, 1,    % 状态4
    6, 0, 1,    % 状态5
    0, 0, 1     % 状态6
|];

离散非连续输入的处理 #

若输入是离散非连续值（如1、3、5），需先将输入值映射为连续索引，再构建转移数组：

% 输入值到连续索引的映射
int: map_input(int x) = 
    if x == 1 then 1
    else if x == 3 then 2
    else 3 endif;

% 构建对应索引的转移数组
set of int: STATE = 0..6;
set of int: INPUT_INDEX = 1..3;
array[STATE, INPUT_INDEX] of int: t = [|
    0, 0, 0,
    2, 3, 1,
    4, 4, 1,
    4, 5, 1,
    6, 6, 1,
    6, 0, 1,
    0, 0, 1
|];

使用时将激励变量通过map_input转换为索引，再传入regular函数。

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