Defines a PLTL formula that can be used in pltl . PLTL formulae must be monitorable, otherwise a compile-time error is raised. Atomic propositions are match patterns.

syntax
( nege)
Represents the negation of formula e. A negation can only appear inside a formula of the following shapes: (conja(negb)), (conj(nega)b), (since(nega)b).

syntax
( disjlr)
Represents the disjunction of two formulae. The free variables of l must be equal to the free variables of r.

syntax
( conjlr)
Represents the conjunction of two formulae. There is a restriction on conjunctions of the following shapes: (conj(nega)b), (conjb(nega)). Namely, the free variables of a must be a subset of the free variables of b.

syntax
( exists(x...+)e)
Given the a sequence of variables, this formula is satisfied when there exists some mapping from the variables to values such that e holds. The free variables of the entire formula is the set of free variables of e minus the quantified xs.

syntax
( previouse)
Requires that e be satisfied at the last time step.

syntax
( sincelr)
Requires that there is some time in the past such that r holds. Since the latest such time (inclusive) until the current time step (exclusive), l holds. The free variables of l must be a subset of the free variables of r.

syntax
( define-pltl-rule (namearg...)body)

Defines a PLTL macro.

syntax
( pltl formula)

Compiles a PLTL formula into a machine .

> (machine-accepts? (pltl (previous(?number? )))'(1a))

#t
> (machine-accepts? (pltl (previous(?number? )))'(1a2))

#f

3Regular Expressions (RE)🔗 i

(require logic/re ) package: logic-lib

syntax
( define-re idr)

r = (complementr)
| (seqr...)
| (unionr...)
| (starr)
| (epsilon)
| (nullset)
| pat

Defines a regular expression that can be used in re .

syntax
( complementr)
Returns the complement of r, i.e., everything accepted by r is no longer accepted and vice versa.

syntax
( seqr...)
Returns the concatenation of the given regular expressions.

syntax
( unionr...)
Returns the union of the given regular expressions.

syntax
( starr)
Returns the Kleene star, i.e. zero or more repetitions, of the given regular expression.

syntax
( epsilon)
A regular expression corresponding to the singleton language with the empty string.

syntax
( nullset)
A regular expression corresponding to the empty language.

syntax
( define-re-rule namebody)
(define-re-rule (namearg...)body)

Defines a regular expression macro.

syntax
( re r)

Compiles a regular expression into a machine.

> (machine-accepts? (re (plus'a))'(aa))

#t
> (machine-accepts? (re (plus'a))'(ab))

#f

4Deterministic Finite Automata (DFA)🔗 i

(require logic/dfa ) package: logic-lib

syntax
( dfa start
(accept...)
[stateevtnext-state]...)

Compiles the given DFA to a machine .

> (define M
(dfa s1(s1)
[s1(equal? 0)s2]
[s1(?even? )s1]
[s2(equal? 0)s1]
[s2(?even? )s2]))
> (machine-accepts? M(list 20402))

#t
> (machine-accepts? M(list 04020))

#f

5Non-deterministic Finite Automata (NFA)🔗 i

(require logic/nfa ) package: logic-lib

syntax
( nfa start
(accept...)
[stateevtnext-state]...)

Compiles the given NFA to a machine .

6Quantified Event Automata (QEA)🔗 i

(require logic/qea ) package: logic-lib

syntax
( qea opt...)

opt = (∀id)
| (∃id)
| (startid)
| (fieldfld-idexpr)
| [->src-idpattgt-idtrans-opt...]

trans-opt = (whenexpr)
| (setfld-idexpr)

Compiles the given QEA to a machine .

> (define Q
(qea
(∀i)
(startstart)
(fieldcurr-bid0)
(fieldmin-bid0)
[-> start(list 'put-up-itemir)item-listed
(set curr-bid0)
(set min-bidr)]
[-> item-listed(list 'bidia)item-listed
(when (> acurr-bid))
(set curr-bida)]
[-> item-listed(list 'selli)sold
(when (> curr-bidmin-bid))]))

> (machine-accepts? Q'((put-up-itema10)
(put-up-itemb50)
(bida100)
(sella)))

#t

> (machine-accepts? Q'((put-up-itema10)
(put-up-itemb50)
(bida5)
(sella)))

#f

syntax
( ∀id)
Universally quantifies the machine over id.

syntax
( ∃id)
Existentially quantifies the machine over id.

syntax
( startid)
Specifies the start state of the QEA.

syntax
( fieldid)
Specifies a field of the QEA.

syntax
[ -> src-idpattgt-idtrans-opt...]
Specifies a transition of the QEA.

syntax
( when expr)
The transition can only occur when expr is #t, where expr can reference fields.

syntax
( set fld-idexpr)
Sets the given field when the transition it taken.

7Stream Logic (SL)🔗 i

(require logic/sl ) package: logic-lib

syntax
( sl (id...)[idexpr]...)

Compiles the given set of stream logic equations to a machine .

> (define S
(sl
(in)
[out(and (out-1#t)(set-first in))]))
> (machine-accepts? S'((in. #t)(in. #t)(in. #t)))

#t
> (machine-accepts? S'((in. #t)(in. #t)(in. #f)))

#f

top ← prev up next →