Commit 206f599b authored by Andrew's avatar Andrew
Browse files

Removed files from BoSy.

parent bf920f30
import Foundation
import Logic
import LTL
import TSCBasic
import TSCUtility
import Utils
public enum LTL2AutomatonConverter: String {
case ltl3ba
case spot
case input
func convert(ltl: LTL) throws -> CoBüchiAutomaton {
switch self {
case .ltl3ba:
return try convertWithLtl3ba(ltl: ltl)
case .spot:
return try convertWithSpot(ltl: ltl)
case .input:
return try useInputFile()
}
}
public static let allValues: [LTL2AutomatonConverter] = [.ltl3ba, .spot, .input]
}
func convertWithLtl3ba(ltl: LTL) throws -> CoBüchiAutomaton {
guard let ltl3baFormatted = ltl.ltl3ba else {
throw "cannot transform LTL to ltl3ba format"
}
let neverClaim = try TSCBasic.Process.checkNonZeroExit(arguments: ["./Tools/ltl3ba", "-f", "(\(ltl3baFormatted))"])
return try parseSpinNeverClaim(neverClaim: neverClaim)
}
func convertWithSpot(ltl: LTL, hoaf: Bool = false) throws -> CoBüchiAutomaton {
guard let ltl3baFormatted = ltl.spot else {
throw "cannot transform LTL to ltl3ba format"
}
let tmp_file = URL(fileURLWithPath: FileManager().currentDirectoryPath).appendingPathComponent("tmp.ltl")
guard let tmp_data = "(\(ltl3baFormatted))".data(using: .utf8) else {
throw "cannot convert ltl data"
}
try tmp_data.write(to: tmp_file)
// var arguments = ["./Tools/ltl2tgba", "-f", "(\(ltl3baFormatted))"]
var arguments = ["./Tools/ltl2tgba", "-F", tmp_file.path]
if hoaf {
arguments += ["-H", "-B"]
} else {
arguments.append("--spin")
}
let output = try TSCBasic.Process.checkNonZeroExit(arguments: arguments)
if hoaf {
return try parse(hoaf: output)
} else {
return try parseSpinNeverClaim(neverClaim: output)
}
}
func useInputFile() throws -> CoBüchiAutomaton {
let in_file = URL(fileURLWithPath: FileManager().currentDirectoryPath).appendingPathComponent("in.spin")
let input = try! String(contentsOf: in_file)
return try parseSpinNeverClaim(neverClaim: input)
}
func parseSpinNeverClaim(neverClaim: String) throws -> CoBüchiAutomaton {
var states: Set<String> = Set()
var rejectingStates: Set<String> = Set()
var initialState: String?
var transitions: [String: [String: Logic]] = [:]
var lastState: String?
// print(neverClaim)
func normalizeStateName(_ name: String) -> String {
name.replacingOccurrences(of: "accept_", with: "").replacingOccurrences(of: "_init", with: "")
}
// print("parse never claim")
for var line in neverClaim.components(separatedBy: "\n") {
line = line.trimmingCharacters(in: NSCharacterSet.whitespacesAndNewlines)
if line.hasPrefix("never") || line.hasPrefix("}") || line.hasPrefix("if") || line.hasPrefix("fi") {
continue
} else if line.hasSuffix(":") {
// state
let origName = String(line[line.startIndex ..< line.index(before: line.endIndex)])
let name = normalizeStateName(String(origName))
transitions[name] = [:]
lastState = name
if origName.hasPrefix("accept_") {
rejectingStates.insert(name)
}
if origName.hasSuffix("_init") {
assert(initialState == nil)
initialState = name
}
states.insert(name)
} else if line.hasPrefix("::") {
// transition
line = line.replacingOccurrences(of: ":: ", with: "")
let components = line.components(separatedBy: " -> goto ")
assert(components.count == 2)
guard let guardStatement = BooleanUtils.parse(string: components[0]) else {
Logger.default().error("could not parse guard expression")
exit(1)
}
let target = normalizeStateName(components[1])
guard let source = lastState else {
exit(1)
}
transitions[source]?[target] = guardStatement
} else if line.contains("skip") {
guard let source = lastState else {
exit(1)
}
transitions[source]?[source] = Literal.True
}
}
assert(initialState != nil)
guard let initial = initialState else {
throw "could not extract initial state from never claim"
}
var automaton = CoBüchiAutomaton(initialStates: [initial],
states: states,
transitions: transitions,
safetyConditions: [:],
rejectingStates: rejectingStates)
automaton.removeRejectingSinks()
automaton.calculateSCC()
return automaton
}
/**
* This function parses the [HOA format](http://adl.github.io/hoaf/),
* but is very limited as it assumes Buchi acceptance
*/
private func parse(hoaf: String) throws -> CoBüchiAutomaton {
var states: Set<String> = Set()
var rejectingStates: Set<String> = Set()
var initialStates: Set<String> = Set()
var transitions: [String: [String: Logic]] = [:]
var ap: [String] = []
var lastState: String?
func toState(_ n: Int) -> String {
"s\(n)"
}
func parseAP(_ line: String) -> [String] {
var aps: [String] = []
var ap: String?
for character in line {
if character == "\"" {
if let apValue = ap {
aps.append(apValue)
ap = nil
} else {
ap = ""
}
} else {
ap?.append(character)
}
}
return aps
}
func getTransition(_ line: String) -> (Logic, String)? {
var formula: String?
var proposition: Int?
var target: Int?
for character in line {
if character == "[" {
formula = ""
} else if character == "]" {
if let prop = proposition {
formula?.append(ap[prop])
proposition = nil
}
target = 0
} else if target == nil {
if character == "t" {
formula = "1"
} else if ["!", "|", "&", " "].contains(character) {
if let prop = proposition {
formula?.append(ap[prop])
proposition = nil
}
formula?.append(character)
} else {
assert(("0" ... "9").contains(character))
guard let number = Int(String(character)) else {
return nil
}
if let prop = proposition {
proposition = prop * 10 + number
} else {
proposition = number
}
}
} else if ("0" ... "9").contains(character) {
if let targetValue = target {
target = targetValue * 10 + Int(String(character))!
}
}
}
guard let formulaValue = formula else {
return nil
}
guard let parsedFormula = BooleanUtils.parse(string: formulaValue) else {
return nil
}
guard let targetValue = target else {
return nil
}
return (parsedFormula, toState(targetValue))
}
var isBody = false
for var line in hoaf.components(separatedBy: "\n") {
line = line.trimmingCharacters(in: NSCharacterSet.whitespacesAndNewlines)
// print(line)
if line.hasPrefix("acc-name:") {
if line != "acc-name: Buchi" {
throw "wrong acceptance condition found in HOAF"
}
} else if line.hasPrefix("Acceptance:") {
if line != "Acceptance: 1 Inf(0)" {
throw "wrong acceptance condition found in HOAF"
}
} else if line.hasPrefix("States:") {
guard let number = Int(line.components(separatedBy: " ")[1]) else {
throw "wrong formating of states in HOAF"
}
(0 ..< number).forEach { states.insert(toState($0)) }
} else if line.hasPrefix("Start:") {
guard let number = Int(line.components(separatedBy: " ")[1]) else {
throw "wrong formating of states in HOAF"
}
initialStates.insert(toState(number))
} else if line.hasPrefix("AP:") {
ap = parseAP(line)
} else if line.hasPrefix("--BODY--") {
isBody = true
} else if isBody, line.hasPrefix("State:") {
let parts = line.components(separatedBy: " ")
guard let number = Int(parts[1]) else {
throw "wrong formating of states in HOAF"
}
lastState = toState(number)
if parts.count > 2, !parts[parts.endIndex.advanced(by: -1)].hasPrefix("\"") {
// is rejecting
rejectingStates.insert(toState(number))
}
transitions[toState(number)] = [:]
} else if isBody, line.hasPrefix("[") {
// transitions
assert(lastState != nil)
guard let (transitionGuard, targetState) = getTransition(line) else {
throw "wrong formating of transition in HOAF"
}
transitions[lastState!]?[targetState] = transitionGuard
}
}
var automaton = CoBüchiAutomaton(initialStates: initialStates,
states: states,
transitions: transitions,
safetyConditions: [:],
rejectingStates: rejectingStates)
automaton.removeRejectingSinks()
automaton.calculateSCC()
return automaton
}
import Automata
import BoundedSynthesis
import CAiger
import Foundation
import Logic
import LTL
import Specification
import TransitionSystem
import TSCBasic
import TSCUtility
import Utils
// MARK: - argument parsing
/**
* Parse specification given by file name.
* If no file name is given, try to read from standard input.
*/
func parseSpecification(fileName: String?) throws -> SynthesisSpecification {
let json: String
if let specificationFileName = fileName {
Logger.default().debug("reading from file \"\(specificationFileName)\"")
json = try String(contentsOfFile: specificationFileName, encoding: .utf8)
} else {
// Read from stdin
Logger.default().debug("reading from standard input")
let standardInput = FileHandle.standardInput
let input = StreamHelper.readAllAvailableData(from: standardInput)
guard let decoded = String(data: input, encoding: .utf8) else {
print("error: cannot read input from stdin")
exit(1)
}
json = decoded
}
guard let specification = SynthesisSpecification.fromJson(string: json) else {
print("error: cannot parse specification")
exit(1)
}
return specification
}
do {
let parser = ArgumentParser(commandName: "BoSyHyper", usage: "specification", overview: "BoSyHyper is a synthesis tool for temporal hyperproperties.")
let specificationFile = parser.add(positional: "specification", kind: String.self, optional: true, usage: "A file containing the specification in BoSy format", completion: .filename)
let environmentOption = parser.add(option: "--environment", kind: Bool.self, usage: "Search for environment strategies instead of system")
let minBoundOption = parser.add(option: "--min-bound", kind: Int.self, usage: "Specify the initial bound (default 1)")
let synthesizeOption = parser.add(option: "--synthesize", kind: Bool.self, usage: "Synthesize implementation after realizability check")
let environmentPaths = parser.add(option: "--paths", kind: Int.self, usage: "Number of paths the environment can use for counterexample strategy (default 2)")
let dqbfOption = parser.add(option: "--dqbf", kind: Bool.self, usage: "Use DQBF encoding")
let args = Array(CommandLine.arguments.dropFirst())
let result = try parser.parse(args)
let searchEnvironment = result.get(environmentOption) ?? false
let initialBound = result.get(minBoundOption) ?? 1
let synthesize = result.get(synthesizeOption) ?? false
let environmentBound = result.get(environmentPaths) ?? 2
let dqbf = result.get(dqbfOption) ?? false
let specification = try parseSpecification(fileName: result.get(specificationFile))
let linear = specification.ltl
let hyperltl = specification.hyperPrenex
// print("linear", linear)
// print("hyper", hyperltl)
if !searchEnvironment {
// build automaton for linear
guard let linearAutomaton = try? CoBüchiAutomaton.from(ltl: !linear, using: .input) else {
Logger.default().error("could not construct automaton")
fatalError()
}
Logger.default().info("Linear automaton contains \(linearAutomaton.states.count) states")
// build the specification automaton for the system player
guard let automaton = try? CoBüchiAutomaton.from(ltl: !hyperltl.ltlBody, using: .spot) else {
Logger.default().error("could not construct automaton")
fatalError()
}
Logger.default().info("Hyper automaton contains \(automaton.states.count) states")
var encoding: BoSyEncoding
if dqbf {
var option = BoSyOptions()
option.solver = SolverInstance.idq
encoding = HyperStateSymbolicEncoding(
options: option,
linearAutomaton: linearAutomaton,
hyperAutomaton: automaton,
specification: specification
)
} else {
encoding = HyperSmtEncoding(
options: BoSyOptions(),
linearAutomaton: linearAutomaton,
hyperAutomaton: automaton,
specification: specification
)
}
for i in initialBound... {
if try encoding.solve(forBound: i) {
print("realizable")
if !synthesize {
exit(0)
}
guard let solution = encoding.extractSolution() else {
fatalError()
}
print((solution as! DotRepresentable).dot)
guard let aiger_solution = (solution as? AigerRepresentable)?.aiger else {
Logger.default().error("could not encode solution as AIGER")
exit(1)
}
let minimized = aiger_solution.minimized
aiger_write_to_file(minimized, aiger_ascii_mode, stdout)
exit(0)
}
}
} else {
// build the specification automaton for environment player
// the environment wins, if it
// 1) either forces a violation of the specification, or
// 2) the system player plays non-deterministic
let body = hyperltl.ltlBody
let pathVariables = hyperltl.pathVariables
guard pathVariables.count == 2 else {
fatalError("more than two path variables is currently not implemented")
}
var counterPaths: [LTLPathVariable] = []
for i in 1 ... environmentBound {
counterPaths.append(LTLPathVariable(name: "env\(i)"))
}
let outputPropositions: [LTLAtomicProposition] = specification.outputs.map { LTLAtomicProposition(name: $0) }
let inputPropositions: [LTLAtomicProposition] = specification.inputs.map { LTLAtomicProposition(name: $0) }
var equalOutputs: [LTL] = []
var equalInputs: [LTL] = []
for (i, path1) in counterPaths.enumerated() {
for path2 in counterPaths[(i + 1)...] {
equalOutputs += outputPropositions.map { ap in LTL.pathProposition(ap, path1) <=> LTL.pathProposition(ap, path2) }
equalInputs += inputPropositions.map { ap in LTL.pathProposition(ap, path1) <=> LTL.pathProposition(ap, path2) }
}
}
let outputEqual: LTL = equalOutputs.reduce(LTL.tt) { val, res in val && res }
let inputEqual: LTL = equalInputs.reduce(LTL.tt) { val, res in val && res }
let deterministic: LTL
switch specification.semantics {
case .mealy:
deterministic = .weakUntil(outputEqual, !inputEqual)
case .moore:
deterministic = .release(!inputEqual, outputEqual)
}
// actually the negated spec of environment
var environmentSpec = deterministic
let pi = pathVariables[0]
let piPrime = pathVariables[1]
for (i, path1) in counterPaths.enumerated() {
for path2 in counterPaths[(i + 1)...] {
environmentSpec &= body.replacePathProposition(mapping: [pi: path1, piPrime: path2])
}
}
for pathVar in counterPaths {
environmentSpec &= linear.addPathPropositions(path: pathVar)
}
guard let specificationAutomaton = try? CoBüchiAutomaton.from(ltl: environmentSpec, using: .spot) else {
Logger.default().error("could not construct automaton")
fatalError()
}
Logger.default().info("Automaton contains \(specificationAutomaton.states.count) states")
let ltlSpecification = SynthesisSpecification(semantics: specification.semantics.swapped,
inputs: outputPropositions.reduce([]) { res, val in res + counterPaths.map { pi in LTL.pathProposition(val, pi).description } },
outputs: inputPropositions.reduce([]) { res, val in res + counterPaths.map { pi in LTL.pathProposition(val, pi).description } },
assumptions: [],
guarantees: [environmentSpec])
var options = BoSyOptions()
options.solver = .rareqs
options.qbfPreprocessor = .bloqqer
options.qbfCertifier = .quabs
let encoding = InputSymbolicEncoding(options: options, automaton: specificationAutomaton, specification: ltlSpecification, synthesize: false)
for i in initialBound... {
if try encoding.solve(forBound: i) {
print("unrealizable")
if !synthesize {
exit(0)
}
guard let solution = encoding.extractSolution() else {
fatalError()
}
print((solution as! DotRepresentable).dot)
guard let aiger_solution = (solution as? AigerRepresentable)?.aiger else {
Logger.default().error("could not encode solution as AIGER")
exit(1)
}
let minimized = aiger_solution.minimized
aiger_write_to_file(minimized, aiger_ascii_mode, stdout)
exit(0)
}
}
}
} catch {
print(error)
exit(1)
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment