进程精化

进程代数里面有个词叫做精化（refine），今天来看看refine是什么意思。

我们说进程P精化了进程Q，也就是P refine Q，当P的trace（迹）是Q的trace（迹）的子集。

我们看一个例子，这里使用工具PAT（Process Analysis Tool）来看一个实例。

test_refine1()=a->b->c->test_refine1();
test_refine2()=a->c->test_refine2()[]a->b->c->test_refine2();
#assert test_refine1() refines test_refine2();
#assert test_refine2() refines test_refine1();

这是我写的一点点代码。

看到两个进程，test_refine1进程比较简单，test_refine2稍微要复杂一些，可以看到test_refine1精化了test_refine2，所以这里的第一个assertion是正确的，第二个是不对的。

我们用PAT进行验证得到如下图：

我们从进程的trace上看到进程的精化，但是进程精化具体是什么含义呢？

这里说说我自己的理解。

我觉得进程的精化就是一个进程可能太复杂，我们需要用一些简单的进程来去实现或者模拟复杂进程里面的主要功能。所以，这样看来，如果A精化B，那么A比B好，因为A简单而且实现了B的大部分功能。