I’m developing a tool for validating sequences of items.
The tool itself needs a map of rules, which are related to keywords extracted from the data-stream sequence. It is a limited subset of linear temporal logic.
I’m trying to express the requirements of the rules in a spec
The current valid rules that I’m able to parse are:
(def valid-rules #{:not-eventually :is-after :relax :next})
My valid demo rule set is:
(def demorules
{:header {:not-eventually :header} ; :header is not allowed to follow :header
:beta {:is-after :header} ; :beta must follow :header
:trailer {:is-after :header ; :trailer must follow :header
:relax [:header] ; :trailer releases constraints from :header
:next :header}}) ; :header must be the next immediate value
I want to make a spec that encodes this information, so that I can validate the consistency of the rules…
What I have for verifying the basic structure is:
(require '[clojure.spec.alpha :as s])
(s/def ::rule.entry (s/or :a keyword? :b (s/+ keyword?)))
(s/def ::rule valid-rules)
(s/def ::rules (s/map-of keyword? (s/map-of ::rule ::rule.entry)))
I would like to express that
if any key X is the subject of a rule, X must also has a top-level entry X’
So these rules are illegal:
(def badrules
[{:X {:not-eventually :Y}}
{:X {:relax [:Y]}}])
I can already do the check for this with
(defn get-rule-entries [rules]
(set (keys rules)))
(defn get-subjects [rules]
(->> (vals rules)
(map vals)
(flatten)
(set)))
(defn subjects-in-rules? [rules]
(every? (get-rule-entries rules) (get-subjects rules)))
which introduces the new rule:
(s/def ::rule-consistent subjects-in-rules?)
But the problem is that there is no good output from (s/explain ::rule-consistent {:X {:not-eventually :Y}})
… just {:X {:not-eventually :Y}} - failed: subjects-in-rules? spec: ::rule-consistent
So I need some help in translating that to a proper spec. I welcome any suggestions
Thanks