Add new LTL representation

The new LTL representation is capable of representing Quantified LTL formulas, such as HyperLTL.

Sources/BoSy/main.swift

@@ -76,35 +76,6 @@ if let semantics = options.semantics {
     specification.semantics = semantics
 }
 
-/*if paths {
-    let unrolling = Unrolling(specification: specification)
-    var i = 1
-    while true {
-        guard let instance = unrolling.getEncoding(forBound: i) else {
-            exit(0)
-        }
-        print("Path length = \(i)")
-        
-        let qcirVisitor = QCIRVisitor(formula: instance)
-        guard let (result, certificate) = quabs(qcir: "\(qcirVisitor)") else {
-            throw BoSyEncodingError.SolvingFailed("solver failed on instance")
-        }
-        //try? "\(qcirVisitor)".write(toFile: "/Users/leander/Desktop/bounded-tree-models/arbiter_15_\(i).qcir", atomically: false, encoding: .ascii)
-        
-        
-        /*let qdimacsVisitor = QDIMACSVisitor(formula: instance)
-        guard let (result, assignments) = rareqs(qdimacs: bloqqer(qdimacs: "\(qdimacsVisitor)")) else {
-            throw BoSyEncodingError.SolvingFailed("solver failed on instance")
-        }*/
-        if result == .SAT {
-            print("realizable")
-            exit(0)
-        }
-        
-        i += 1
-    }
-}*/
-
 //Logger.default().info("inputs: \(specification.inputs), outputs: \(specification.outputs)")
 //Logger.default().info("assumptions: \(specification.assumptions), guarantees: \(specification.guarantees)")
 

Sources/LTL/LTL+CustomStringConvertible.swift

@@ -0,0 +1,43 @@
+
+extension LTL: CustomStringConvertible {
+
+    public var description: String {
+        switch self {
+        case .atomicProposition(let ap):
+            return ap.description
+        case .pathProposition(let ap, let path):
+            return "\(ap)[\(path)]"
+        case .application(let function, parameters: let parameters):
+            switch function.arity {
+            case 0:
+                return "\(function)"
+            case 1:
+                return "\(function) \(parameters[0])"
+            case 2:
+                return "\(parameters[0]) \(function) \(parameters[1])"
+            default:
+                fatalError()
+            }
+        case .pathQuantifier(let quant, parameters: let parameters, body: let body):
+            return "\(quant) \(parameters.map(String.init(describing:)).joined(separator: " ")). \(body)"
+        }
+    }
+}
+
+extension LTLPathVariable: CustomStringConvertible {
+    public var description: String {
+        return name
+    }
+}
+
+extension LTLAtomicProposition: CustomStringConvertible {
+    public var description: String {
+        return name
+    }
+}
+
+extension LTLFunction: CustomStringConvertible {
+    public var description: String {
+        return symbol
+    }
+}

Sources/LTL/LTL+Hashable.swift

@@ -0,0 +1,40 @@
+
+extension LTLFunction: Hashable {
+    public var hashValue: Int {
+        return symbol.hashValue ^ arity.hashValue
+    }
+
+    public static func ==(lhs: LTLFunction, rhs: LTLFunction) -> Bool {
+        return lhs.symbol == rhs.symbol && lhs.arity == rhs.arity
+    }
+}
+
+extension LTLAtomicProposition: Equatable {
+    public static func ==(lhs: LTLAtomicProposition, rhs: LTLAtomicProposition) -> Bool {
+        return lhs.name == rhs.name
+    }
+}
+
+extension LTLPathVariable: Equatable {
+    public static func ==(lhs: LTLPathVariable, rhs: LTLPathVariable) -> Bool {
+        return lhs.name == rhs.name
+    }
+}
+
+extension LTL: Equatable {
+    public static func == (lhs: LTL, rhs: LTL) -> Bool {
+        switch (lhs, rhs) {
+        case (.atomicProposition(let lhs), .atomicProposition(let rhs)):
+            return lhs == rhs
+        case (.pathProposition(let lhs, let lhsPath), .pathProposition(let rhs, let rhsPath)):
+            return lhs == rhs && lhsPath == rhsPath
+        case (.application(let lhsFun, let lhsParameters), .application(let rhsFun, parameters: let rhsParameters)):
+            return lhsFun == rhsFun && lhsParameters == rhsParameters
+        case (.pathQuantifier(let lhsQuant, let lhsParamaters, let lhsBody), .pathQuantifier(let rhsQuant, parameters: let rhsParameters, body: let rhsBody)):
+            return lhsQuant == rhsQuant && lhsParamaters == rhsParameters && lhsBody == rhsBody
+        default:
+            return false
+        }
+    }
+}
+

Sources/LTL/LTL+Operators.swift

@@ -0,0 +1,29 @@
+
+// We define operators to make working with LTL easier
+
+// FIXME: check which precedence is correct
+infix operator =>
+
+extension LTL {
+
+    public static func && (lhs: LTL, rhs: LTL) -> LTL {
+        return .application(.and, parameters: [lhs, rhs])
+    }
+
+    public static func || (lhs: LTL, rhs: LTL) -> LTL {
+        return .application(.or, parameters: [lhs, rhs])
+    }
+
+    public static prefix func ! (ltl: LTL) -> LTL {
+        return .application(.negation, parameters: [ltl])
+    }
+
+    public static func => (lhs: LTL, rhs: LTL) -> LTL {
+        return .application(.implies, parameters: [lhs, rhs])
+    }
+
+    public static func until(_ lhs: LTL, _ rhs: LTL) -> LTL {
+        return .application(.until, parameters: [lhs, rhs])
+    }
+
+}