不用真实模型也能验证状态机

import java.util.*;
public class Main {
    record Machine(int[][] next,String[] output){}
    static int validate(Machine m){
        if(m.next().length==0||m.output().length!=m.next().length)throw new IllegalArgumentException("shape");
        int events=m.next()[0].length;
        for(int[] row:m.next()){if(row.length!=events)throw new IllegalArgumentException("alphabet");for(int s:row)if(s<0||s>=m.next().length)throw new IllegalArgumentException("target");}
        for(String out:m.output())Objects.requireNonNull(out);return events;
    }
    static Optional<List<Integer>> difference(Machine a,Machine b){
        int events=validate(a);if(validate(b)!=events)throw new IllegalArgumentException("alphabet mismatch");
        int nb=b.next().length,total=Math.multiplyExact(a.next().length,nb);if(total>1000000)throw new IllegalArgumentException("state budget");
        int[] prev=new int[total],via=new int[total];Arrays.fill(prev,-2);prev[0]=-1;
        Deque<Integer> q=new ArrayDeque<>();q.add(0);
        while(!q.isEmpty()){
            int pair=q.removeFirst(),x=pair/nb,y=pair%nb;
            if(!a.output()[x].equals(b.output()[y])){
                List<Integer> path=new ArrayList<>();for(int p=pair;prev[p]!=-1;p=prev[p])path.add(via[p]);
                Collections.reverse(path);return Optional.of(path); // 空路径也是起点差异的有效证据。
            }
            for(int e=0;e<events;e++){
                int next=a.next()[x][e]*nb+b.next()[y][e];
                if(prev[next]==-2){prev[next]=pair;via[next]=e;q.addLast(next);} // 每个二元组只入队一次。
            }
        }
        return Optional.empty(); // 只证明给定有限抽象和事件集合下无差异。
    }
    static void eq(Object e,Object a){if(!e.equals(a))throw new AssertionError(a);}
    public static void main(String[] args){
        Machine a=new Machine(new int[][]{{0,1},{1,1}},new String[]{"R","D"});
        Machine b=new Machine(new int[][]{{0,0},{1,1}},new String[]{"R","D"});
        eq(Optional.of(List.of(1)),difference(a,b));eq(Optional.empty(),difference(a,a));
        eq(Optional.of(List.of()),difference(new Machine(new int[][]{{0}},new String[]{"A"}),new Machine(new int[][]{{0}},new String[]{"B"})));
        Machine c=new Machine(new int[][]{{1,0},{1,2},{2,2}},new String[]{"R","R","D"});
        Machine d=new Machine(new int[][]{{1,0},{1,1},{2,2}},new String[]{"R","R","D"});
        eq(Optional.of(List.of(0,1)),difference(c,d));
        try{difference(new Machine(new int[][]{{2}},new String[]{"R"}),a);throw new AssertionError();}catch(IllegalArgumentException expected){}
        System.out.println("PASS 5 tests");
    }
}