Specification Files

The user may specify a set of SLS objects (swords, slanguages, sexpressions) related to a common alphabet of letters in a specification file whose name should have the extension .txt.

An SLS specification file starts with the definition of a signature, eventually followed by th e definition of a set of variables. Next we may have in any order definitions of TRSs, automata, termsets, each one of them associated with a distinct name.

Example: trains.txt

Problem trains
 ([{a,b,e}] . ([{a}] X [{b}] X [{e}]))
 (([{a}] X [{b}]) . [{a}{b}])
 ((([{a}] X [{c}]) . [{a}{c}{d}{d}]) U (([{a}] X [{c}]) . [{a,c}{d}{d}]))
 ([{b}{b,d,f}] . ([{f}] X [{d}]))
 (([{e}] X [{d}]) . [{d,e}])

Sword [{a}{{a}]
Lexpr ([{a}{a}] X [{b}{b}])
Lexpr ([{a,b}] J [{b_1,c}])