From 36b59b5baf8dc3b5f246d378a1a0ad263b0b0177 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 29 Apr 2018 17:16:25 +0100
Subject: [PATCH] Universal K support

---
 mc.cc | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/mc.cc b/mc.cc
index 95c82c3..9300923 100644
--- a/mc.cc
+++ b/mc.cc
@@ -350,6 +350,10 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
     auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
     return statesNK(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_id) * *reach;
   }
+  else if (oper == RSCTLK_UK) {
+    auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
+    return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach);
+  }
 
   assert(0); // Should never happen
   return BDD_FALSE;