有偿求助pl0编译到nusmv（一个模型检测侧软件，语言很简单）

毕设需要写一个 compiler， 从pl0到 nusmv。 现有一个从pl0到Tla的翻译器。
nusmv和tla都是模型检测软件，都是自己的语言，但是很简单。pl0到tla的那个翻译器的前半部分包括词法什么的abstract tree 可以直接用，相当于前端弄好了，需要些后端生成nusmv文件。 只要能过两个文件的pass就可以。具体内容价钱 请加qq详谈。