Commit 3f25f7b365de7bb282b1de08818ba440b704a390 - cafeobj

* There can be a case in which expansion of :m-and by 'and-also' causes normalization to be failed. So, revert to original expansion by 'and'. * Now there is a hidden swich 'm-and-also', if on :m-and is expanded by 'and-also'. default is off. * Search predicate needs cases the target term of 'reduce' command contains variables. To adopt this, system does not replace variables in target term with constants. tswd 10 years ago

17 changed file(s) with 642 addition(s) and 217 deletion(s). Raw diff Collapse all Expand all

-0

.gitignore less more

12	12	*.ind
13	13	*.out
14	14	*.toc
	15	*.diff
15	16	.\#*
16	17	\#*
17	18	*.cache

-1

cafeobj/defcommand.lisp less more

21	21	;;; commands which can apper at top-level --------------------------------------
22	22	;;;
23	23
24		(defcom ("mod" "module" "module" "mod" "module!" "mod!" "sys:mod!")
	24	(defcom ("mod" "module" "module" "mod" "module!" "mod!" "sys:mod!" "sys:module!" "sys:mod" "sys:module")
25	25	"declares module.~%module <Name> [<Parameters>] [<PrincipalSort>] { <ModuleBody> }."
26	26	:toplevel-declaration
27	27	process-module-declaration-form

-1

cafeobj/trans-decl.lisp less more

379	379	(return-from process-operator-declaration-form nil)))
380	380	(when (equal '("_") pat)
381	381	(with-output-chaos-warning ()
382		(princ "operator pattern is just _, declaration ignored.")
	382	(format t "operator pattern is just _, declaration ignored. ~s" e)
383	383	(return-from process-operator-declaration-form nil)))
384	384	(let ((arity (mapcar #'(lambda (x)
385	385	(process-sort-reference-form x))

-2

chaos/cafein/rengine.lisp less more

1685	1685	;;
1686	1686	(setq new-rhs (make-right-assoc-normal-form-with-sort-check
1687	1687	(if (eq mandor :m-and)
1688		bool-and-also
1689		bool-or-else)
	1688	m-and-op
	1689	m-or-op)
1690	1690	rhs-list))
1691	1691	#\|\|
1692	1692	(setq new-axiom (make-rule :lhs (rule-lhs rule)

-0

chaos/eval/eval-ast2.lisp less more

151	151	(when (or (null (term-sort term))
152	152	(sort<= (term-sort term) syntax-err-sort chaos-sort-order))
153	153	(return-from perform-reduction* nil))
	154	#\|\|
154	155	(setq term (replace-variables-with-toc
155	156	term
156	157	"The target term contains variables, system replaces them with 'constants'." ))
	158	\|\|#
157	159	(when rewrite-stepping (setq steps-to-be-done 1))
158	160	(when show-stats
159	161	(setq time2 (get-internal-run-time))

+63

-112

chaos/term-parser/parse-engine.lisp less more

12	12
13	13	;;; NOTE PARSING ALGORITHM is BASED ON OBJ3 interpreter of SRI International.
14	14	;;; Copyright 1988,1991 SRI International.
15
16		;;; (defvar on-parse-debug nil)
17	15
18	16	;;;*********************************
19	17	;;; PARSE DICTIONARY BASIC ROUTINES

133	131	(declare (type list res))
134	132	(if res
135	133	(cdr res)
136		(progn
137		(push (cons (variable-name term) ;; (variable-copy term)
138		term)
139		parse-variables)
140		term))))
	134	(progn
	135	(push (cons (variable-name term) ;; (variable-copy term)
	136	term)
	137	parse-variables)
	138	term))))
141	139	(if (term-is-application-form? term)
142	140	(@create-application-form-term (term-head term)
143	141	(term-sort term)
144	142	(mapcar #'(lambda (x)
145		(simple-copy-term-sharing-variables
146		x
147		dict))
	143	(simple-copy-term-sharing-variables x dict))
148	144	(term-subterms term)))
149		(simple-copy-term term)
150		)))
151
	145	(simple-copy-term term))))
152	146
153	147	(defun get-qualified-op-pattern (tok &optional (module (or current-module
154	148	last-module)))

161	155	(destruct-op-name
162	156	(subseq expr (1+ pos)))))
163	157	expr)))
164		;;
165	158	(parse-opref (expr)
166	159	(declare (type string expr))
167	160	(let ((val (destruct-op-name expr)))

172	165	(let ((pos (position #\. name)))
173	166	(if (and pos (< 0 pos) (< (1+ pos) (length name)))
174	167	;; "foo.qualifier"
175		(values (cons (subseq name 0 pos)
176		(cdr val))
	168	(values (cons (subseq name 0 pos) (cdr val))
177	169	(subseq name (1+ pos)))
178	170	(return-from get-qualified-op-pattern nil))))))
179	171	(find-qual-operators-2 (name module context)
180		(let ((modval (find-module-in-env-ext
181		(canonicalize-simple-module-name module)
182		context
183		:no-error)))
	172	(let ((modval (find-module-in-env-ext (canonicalize-simple-module-name module)
	173	context
	174	:no-error)))
184	175	(if (module-p modval)
185	176	(find-operators-in-module-no-number name modval nil t)
186	177	(with-output-chaos-error ('invalid-context)
187		(format t "module ~a is not available in the current context." module)))
188		))
189		)
190		;;
	178	(format t "module ~a is not available in the current context." module))))))
191	179	(let ((info nil)
192	180	(res nil))
193	181	(multiple-value-bind (name qual)
194	182	(parse-opref tok)
195		(setq info (find-qual-operators-2 name
196		qual
197		module))
	183	(setq info (find-qual-operators-2 name qual module))
198	184	(dolist (i info)
199	185	(if (cdr (opinfo-methods i))
200	186	(push (cadr (opinfo-methods i)) res)
201		(push (car (opinfo-methods i)) res)))
	187	(push (car (opinfo-methods i)) res)))
202	188	(values res name)))))
203	189
204	190	(defun parser-is-more-general-one (obj lst)

339	325	(progn
340	326	;; check name, if it start with `, we make
341	327	;; pseudo variable
342		(if (eql #\` (char (the simple-string
343		(string var-name))
344		0))
345		(setf var (make-pvariable-term sort
346		var-name))
347		(setf var (make-variable-term sort
348		var-name)))
	328	(if (eql #\` (char (the simple-string (string var-name)) 0))
	329	(setf var (make-pvariable-term sort var-name))
	330	(setf var (make-variable-term sort var-name)))
349	331	(push (cons var-name var) parse-variables)))
350	332	(if old-var
351	333	(progn

364	346	(when svar
365	347	(with-output-chaos-error ()
366	348	(format t "Static variable ~s already used before in the same context" var-name)))
367
368	349	(push var res)
369	350	#\|\|
370	351	(when (err-sort-p (variable-sort var))

405	386	(let ((real-res nil))
406	387	(dolist (r res)
407	388	(cond ((term? r)
408		(when (parser-in-same-connected-component
409		(term-sort r)
410		sort-constraint
411		current-sort-order)
	389	(when (parser-in-same-connected-component (term-sort r)
	390	sort-constraint
	391	current-sort-order)
412	392	(push r real-res)))
413	393	((method-p r)
414		(when (parser-in-same-connected-component
415		(method-coarity r) sort-constraint
416		current-sort-order)
	394	(when (parser-in-same-connected-component (method-coarity r)
	395	sort-constraint
	396	current-sort-order)
417	397	(push r real-res)))
418	398	(t (push r real-res))))
419	399	(when real-res
420	400	(setq res real-res))))
421		;;
422	401	(let ((result nil))
423	402	(loop
424	403	(unless res (return))
425	404	(let ((p (pop res)))
426	405	(unless (parser-is-more-general-one p res)
427		(push p result)))
428		)
	406	(push p result))))
429	407	(setq res (nreverse result)))
430		;;
431	408	(when on-parse-debug
432	409	(format t "~& : sort constraint = ")
433	410	(print-chaos-object sort-constraint)
434	411	(format t "~& : result info = ~s" res)
435	412	(print-chaos-object res))
436		(values res (car mod-token))
437		))
	413	(values res (car mod-token))))
438	414
439	415	(defun dictionary-delete-vars (lst)
440	416	(declare (type list lst))

480	456	(if (term-is-variable? e)
481	457	'variable
482	458	(if (term-is-builtin-constant? e)
483		'builtin
484		(if (term-is-lisp-form? e)
485		'lisp-form
486		'normal-term))))
	459	'builtin
	460	(if (term-is-lisp-form? e)
	461	'lisp-form
	462	'normal-term))))
487	463	((operator-method-p e)
488	464	(operator-syntactic-type (method-operator e)))
489	465	(t 'ast)))

655	631	(print-chaos-object terletox-sublist-prime))
656	632	;;
657	633	(nconc terletox-sublist-prime
658		(parser-continue terletox0 module level-constraint sort-constraint)
659		)
660		))
	634	(parser-continue terletox0 module level-constraint sort-constraint))))
661	635
662	636	;;; PARSER-CONTINUE :
663	637	;;; ( ( ChaosTerm . PrecedenceLevel ) . TokenList )

822	796	module)))
823	797	(if (null first-result-list)
824	798	nil ;return an empty solution
825		(parser-continuing first-result-list
826		module
827		level-constraint
828		sort-constraint))))
	799	(parser-continuing first-result-list
	800	module
	801	level-constraint
	802	sort-constraint))))
829	803
830	804	;;; op parser-finish-term-for-operator :
831	805	;;; TokenList

868	842	(arg-acc-list-prime ;possibly nil
869	843	(parser-collect-arguments arg-acc-list
870	844	module
871		rest-form
872		)))
	845	rest-form)))
873	846	(if (null arg-acc-list-prime)
874	847	;; illegal
875	848	;; (parser-make-terms late-juxt-operator arg-acc-list module)
876	849	nil
877		(parser-make-terms late-juxt-operator arg-acc-list-prime module))))
	850	(parser-make-terms late-juxt-operator arg-acc-list-prime module))))
878	851
879	852	;;; op parser-get-term :
880	853	;;; TokenList -- not empty !

903	876	(if (null token-list-prime)
904	877	nil ;return an empty set of solutions
905	878	(parser-get-rest-of-parenthesized-expr token-list-prime
906		module
907		)))
	879	module)))
908	880	(;; (member token1 '( ")" "," ) :test #'equal)
909	881	(equal token1 ")")
910	882	;;* Unacceptable reserved tokens

915	887	token-list-prime
916	888	module
917	889	level-constraint
918		sort-constraint
919		)))))
	890	sort-constraint)))))
920	891
921	892	;;; op parser-get-rest-of-parenthesized-expr :
922	893	;;; TokenList -- not empty !

965	936	(and (eql #\: fst)
966	937	(not (equal (cadr token-list) ":is"))
967	938	(dolist (in info t)
968		(when (member (object-syntactic-type
969		in)
970		'(antefix juxtaposition
971		latefix))
972		(return nil))))
973		))
	939	(when (member (object-syntactic-type in)
	940	'(antefix juxtaposition latefix))
	941	(return nil))))))
974	942	;; !! might modify this last condition a bit
975	943	(multiple-value-bind (terms toks)
976	944	(parser-scan-qualification chaos-terms

997	965	(let ((tokens (if (equal (car token-list) ":")
998	966	(cdr token-list)
999	967	(cons (subseq (the simple-string (car token-list)) 1)
1000		(cdr token-list)))
1001		)
	968	(cdr token-list))))
1002	969	(res nil)
1003	970	qualifier
1004	971	rest)

1134	1101	(setq terletox-list-prime ; accumulate
1135	1102	(nconc res terletox-list-prime))
1136	1103	(return-from get-term-for-regular-token
1137		(nconc res terletox-list-prime))))))
1138		)))))
	1104	(nconc res terletox-list-prime)))))))))))
1139	1105
1140	1106	;;; op get-term-for-op-var :
1141	1107	;;; Operator(Mehotd) + Variable

1145	1111	;;; ->
1146	1112	;;; LIST[ ( ( ChaosTerm . PrecedenceLevel ) . TokenList ) ] .
1147	1113	;;; -- possibly empty
1148
1149	1114	(defun get-term-for-op-var (op-var token-list module level-constraint
1150	1115	&optional sort-constraint)
1151	1116	(declare (type t op-var)

1169	1134	;; 2. Antefix
1170	1135	(antefix
1171	1136	;; is precedence of antefix operator acceptable ?
1172		(unless (<= (the fixnum
1173		(get-method-precedence op-var))
	1137	(unless (<= (the fixnum (get-method-precedence op-var))
1174	1138	level-constraint)
1175	1139	(return-from get-term-for-op-var nil))
1176	1140	(let ((res (get-term-from-antefix-operator op-var token-list module)))
1177		res)
1178		)
	1141	res))
	1142
1179	1143	;; 3. Ast
1180	1144	(ast
1181	1145	(get-term-from-ast-operator op-var token-list module))
1182	1146
1183	1147	;; 4. token does not belong to sub-formula.
1184		;;
1185		(otherwise nil) ;return a void solution
1186		))
	1148	;; return a void solution
	1149	(otherwise nil)))
1187	1150
1188	1151	;;; op get-term-from-antefix-operator :
1189	1152	;;; Operator -- must be antefix !

1202	1165	(arg-acc-list (list (cons nil token-list))) ;initialization
1203	1166	(arg-acc-list-prime (parser-collect-arguments arg-acc-list
1204	1167	module
1205		rest-form
1206		)))
	1168	rest-form)))
1207	1169	(if (null arg-acc-list-prime)
1208	1170	;; return a void answer
1209	1171	;; (parser-make-terms method arg-acc-list module)

1294	1256	op-var
1295	1257	module
1296	1258	level-constraint)
1297		late-juxt-op-list-prime)
1298		))))
	1259	late-juxt-op-list-prime)))))
1299	1260
1300	1261	;;; op choose-operators :
1301	1262	;;; ( ChaosTerm . PrecedenceLevel )

1363	1324	(get-method-precedence juxt-op))
1364	1325	level-constraint)
1365	1326	(parser-check-operator term-level0 juxt-op module))
1366		(setq res (cons juxt-op res)))
1367		)))))
	1327	(setq res (cons juxt-op res))))))))
1368	1328
1369	1329	;;; op choose-latefix-operators :
1370	1330	;;; ( ChaosTerm . PrecedenceLevel )

1379	1339	;;; - able to accept term-level0 as a first argument
1380	1340	;;; (check sort and precedence)
1381	1341
1382		(defun choose-latefix-operators (term-level0 latefix-operator module
1383		level-constraint)
	1342	(defun choose-latefix-operators (term-level0 latefix-operator module level-constraint)
1384	1343	(declare (type t term-level0)
1385	1344	(type method latefix-operator)
1386	1345	(type module module)

1391	1350	latefix-operator
1392	1351	module))
1393	1352	(list latefix-operator)
1394		nil ;return a void answer
1395		))
	1353	;; return a void answer
	1354	nil))
1396	1355
1397	1356	;;; op parser-check-operator :
1398	1357	;;; ( ChaosTerm . PrecedenceLevel )

1414	1373	(first-arg-constraints (car form))
1415	1374	(first-arg-level-constraint (or (cadr first-arg-constraints) 0))
1416	1375	(first-arg-sort-constraint (car (method-arity late-juxt-op)))
1417		(sort-order (module-sort-order module))
1418		)
	1376	(sort-order (module-sort-order module)))
1419	1377	(declare (type fixnum level0 first-arg-level-constraint))
1420	1378	(and (<= level0 first-arg-level-constraint)
1421	1379	(parser-in-same-connected-component sort0

1464	1422	(parser-collect-one-argument arg-acc-list-prime
1465	1423	module
1466	1424	(cadr form-item)
1467		(cddr form-item)))
1468		)
1469
	1425	(cddr form-item))))
1470	1426	;; 3. collect varargs. --- to be done.
1471	1427	((argument* argument+)
1472	1428	(let ((limit 256)) ; for avoiding infinite loop

1492	1448	(parser-collect-one-argument arg-acc-list-prime
1493	1449	module
1494	1450	(cadr form-item)
1495		(cddr form-item))))))))
1496		)
1497		;;
	1451	(cddr form-item)))))))))
1498	1452	(if (null arg-acc-list-prime)
1499	1453	(return nil)
1500	1454	;; to avoid unnecessary additional loops, and to avoid calling
1501	1455	;; either parser-scan-token or
1502	1456	;; parser-collect-one-argument with void arguments.
1503		))
	1457	))
1504	1458	;; a bit optimization
1505	1459	#\|\|
1506	1460	(let ((res nil))

1760	1714	(eq ,sort cosmos-sort)
1761	1715	(eq (sort-type ,sort) '%err-sort))))
1762	1716	(flet ((make-form (sort method arg-list)
1763		(make-applform sort method arg-list)
1764		))
	1717	(make-applform sort method arg-list)))
1765	1718	(let ((result nil))
1766	1719	(if fill-rc-attribute
1767	1720	(let ((attrpos nil)

1829	1782	;; special treatment of generic operators
1830	1783	(when (eq (term-head result) bool-if)
1831	1784	(set-if-then-else-sort result))
1832		result
1833		))))
	1785	result))))
1834	1786
1835	1787	(defun replace-class-id-with-var (cr-sort arg-list)
1836	1788	(declare (type sort* cr-sort)

1971	1923	;; other binary universal operators
1972	1924	(parser-in-same-connected-component (first sort-list)
1973	1925	(second sort-list)
1974		so))
1975		)
	1926	so)))
1976	1927	t)))
1977	1928
1978	1929	;;; op are-well-defined-terms :

1986	1937	(let ((result t))
1987	1938	(dolist (chaos-term chaos-term-list result)
1988	1939	(if (term-ill-defined chaos-term)
1989		(return nil) ;abort looping and return false
1990		))))
	1940	;; abort looping and return false
	1941	(return nil)))))
1991	1942
1992	1943
1993	1944	;;; EOF

+10

-0

chaos/tools/set.lisp less more

182	182	("debug" ("exec") parity cexec-debug "" nil nil t)
183	183	("debug" ("meta") parity debug-meta "" nil nil t)
184	184	;;
	185	("m-and-also" () general nil "" set-m-and-also nil t)
185	186	))
186	187
187	188	(defun set-chaos-switch (which value)

404	405	(setq path (car path)))
405	406	(setq user-bool path)))
406	407
	408	;;;
	409	(defun set-m-and-also (value)
	410	(cond ((string= (car value) "on")
	411	(setq m-and-op bool-and-also)
	412	(setq m-or-op bool-or-else))
	413	(t
	414	(setq m-and-op bool-and)
	415	(setq m-or-op bool-or-else))))
	416
407	417	;;; EOF
408	418

-0

comlib/globals.lisp less more

458	458	(defvar bool-or-else 'void)
459	459	(defvar bool-iff 'void)
460	460	(defvar eql-op 'void)
	461	(defvar m-and-op nil)
	462	(defvar m-or-op nil)
461	463
462	464	;;; RWL
463	465	;;;-----------------------------------------------------------------------------

-1

configure less more

1694	1694	VERSION=1.4
1695	1695	VMINOR=.13
1696	1696	VMEMO=PigNose0.99
1697		PATCHLEVEL=alpha-1
	1697	PATCHLEVEL=a2
1698	1698
1699	1699
1700	1700

-1

configure.in less more

7	7	VERSION=1.4
8	8	VMINOR=.13
9	9	VMEMO=PigNose0.99
10		PATCHLEVEL=alpha-1
	10	PATCHLEVEL=a2
11	11	AC_SUBST(PACKAGE)
12	12	AC_SUBST(VERSION)
13	13	AC_SUBST(VMINOR)

-1

lib/lib/bool.cafe less more

55	55	(let* ((iff (find-operator '("_" "iff" "_") 2 bool-module))
56	56	(iff-meth (lowest-method* (car (opinfo-methods iff)))))
57	57	(setq bool-iff iff-meth))
58		)))
	58	(setq m-and-op bool-and)
	59	(setq m-or-op bool-or))))
59	60
60	61	-- **
61	62	-- ** MODULE BOOL

+24

-30

lib/lib/metalevel.cafe less more

0	0	**
1	1	** CafeOBJ MetaLevel Core
2	2	**
3		mod! :SET(X :: TRIV) {
	3	sys:mod! :SET(X :: TRIV) {
4	4	protecting (BOOL)
5	5	protecting (NAT)
6	6	[ Elt.X < NeSet < Set ]

68	68	eq S psubset S' = S =/= S' and-also S subset S' .
69	69	}
70	70
71		mod! :LIST(X :: TRIV) {
	71	sys:mod! :LIST(X :: TRIV) {
72	72	protecting (NAT)
73	73	[ Elt.X < NeList < List ]
74	74

119	119	eq $size(E L, C) = $size(L, C + 1) .
120	120	}
121	121
122		mod! NAT-LIST {
123		protecting (:LIST(NAT) * {sort NeList -> NeNatList, sort List -> NatList})
124		}
125
126		mod! QID-LIST {
127		protecting (:LIST(QID) * {sort NeList -> NeQidList, sort List -> QidList})
128		}
129
130		mod! QID-SET {
131		protecting (:SET(QID) * {sort NeSet -> NeQidSet, sort Set -> QidSet})
132		}
	122	sys:mod! NAT-LIST {protecting (:LIST(NAT) * {sort NeList -> NeNatList, sort List -> NatList})}
	123
	124	sys:mod! QID-LIST {protecting (:LIST(QID) * {sort NeList -> NeQidList, sort List -> QidList})}
	125
	126	sys:mod! QID-SET {protecting (:SET(QID) * {sort NeSet -> NeQidSet, sort Set -> QidSet})}
133	127
134	128	**
135	129	** META-TERM

252	246	[ Qid < ModuleExpression ]
253	247	op _+_ : ModuleExpression ModuleExpression -> ModuleExpression {ctor assoc comm}
254	248	op _*{_} : ModuleExpression RenamingSet -> ModuleExpression {ctor prec: 39}
255		op _(_) : ModuleExpression ParameterList -> ModuleExpression {ctor prec: 37}
	249	op _[_] : ModuleExpression ParameterList -> ModuleExpression {ctor prec: 37}
256	250
257	251	** parameter declarations
258	252	[ ParameterDecl < NeParameterDeclList < ParameterDeclList ]

296	290
297	291	** conditions
298	292	[ EqCondition < Condition ]
299		op nil : -> EqCondition {ctor}
300		op _=_ : Term Term -> EqCondition {ctor prec: 71}
301		op _:_ : Term Sort -> EqCondition {ctor prec: 71}
302		op _:=_ : Term Term -> EqCondition {ctor prec: 71}
303		op _=>_ : Term Term -> Condition {ctor prec: 71}
304		op _/\_ : EqCondition EqCondition -> EqCondition {ctor assoc id: nil prec: 73}
305		op _/\_ : Condition Condition -> Condition {ctor assoc id: nil prec: 73}
	293	op nil : -> EqCondition {ctor}
	294	op _=_ : Term Term -> EqCondition {ctor prec: 71}
	295	op (_:_) : Term Sort -> EqCondition {ctor prec: 71}
	296	op (_:=_): Term Term -> EqCondition {ctor prec: 71}
	297	op _=>_ : Term Term -> Condition {ctor prec: 71}
	298	op _/\_ : EqCondition EqCondition -> EqCondition {ctor assoc id: nil prec: 73}
	299	op _/\_ : Condition Condition -> Condition {ctor assoc id: nil prec: 73}
306	300
307	301	** equations
308	302	[ Equation < EquationSet ]

321	315	eq R:Rule R:Rule = R:Rule .
322	316
323	317	** modules
324		[ FModule < SModule < Module ]
325		[ FTheory < STheory < Module ]
	318	[ FModule Theory LModule < Module ]
326	319	[ Qid < Header ]
327	320
328	321	op _[_] : Qid ParameterDeclList -> Header {ctor}
329		op module!_{_[_]__} : Header ImportList SubsortDeclSet OpDeclSet EquationSet
	322	op module!_{_[_]____} : Header ImportList SortSet SubsortDeclSet OpDeclSet EquationSet RuleSet
330	323	-> FModule {ctor}
331
332		op module_{_[_]___} : Header ImportList SubsortDeclSet OpDeclSet EquationSet RuleSet
333		-> SModule {ctor}
334		op [_] : Qid -> Module .
	324	op module_{_[_]____} : Header ImportList SortSet SubsortDeclSet OpDeclSet EquationSet RuleSet
	325	-> LModule {ctor}
	326	op module*_{_[_]____} : Header ImportList SortSet SubsortDeclSet OpDeclSet EquationSet RuleSet
	327	-> Theory {ctor}
	328	** op [_] : Qid -> Module .
335	329	** eq [Q:Qid] = (module* Q:Qid { including(Q:Qid)
336	330	** [ none ] none none none none none }) .
337	331

350	344
351	345	eof
352	346	op getName : Module -> Qid .
353		eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
354		eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .
	347	eq getName(mod! Q {IL sorts SS . SSDS OPDS MAS EQS }) = Q .
	348	eq getName(mod! Q {IL sorts SS . SSDS OPDS MAS EQS RLS }) = Q .
355	349	eq getName(fmod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
356	350	eq getName(mod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .
357	351	eq getName(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = Q .

-67

~~load-source.lisp~~ less more

0		(in-package :user)
1
2		(defparameter top-files
3		'("." "chaos-package" "version"))
4		(defparameter comlib
5		'("comlib" "globals" "macros" "print-utils" "message"
6		"error" "misc" "string" "list" "dag" "fsys" "tree-display"
7		"lex" "reader"))
8		(defparameter primitives
9		'("chaos/primitives"
10		"term" "defterm" "bobject2" "absntax" "script" "op-theory" "bmodexp"
11		"bmodule2" "bview2" "parse-modexp" "normodexp"
12		"bsort" "boperator" "baxioms" "gen-eval" "gen-print"
13		"context" "term-utils" "substitution" "find" "print-object"))
14		(defparameter term-parser
15		'("chaos/term-parser"
16		"parse-engine" "parse-top"))
17		(defparameter e-match
18		'("chaos/e-match"
19		"match-utils" "match-system" "match-e" "match-idem"
20		"match-z" "match-a" "match-c" "match-az" "match-cz"
21		"match-ac" "match-acz" "match" "match2"))
22		(defparameter construct
23		'("chaos/construct"
24		"sort" "operator" "variable" "match-method" "axiom" "gen-rule"
25		"cr" "rwl" "beh" "module" "trs"))
26		(defparameter decafe
27		'("chaos/decafe"
28		"mutils" "modmorph" "mrmap" "meval" "view" "mimport"))
29		(defparameter cafein
30		'("chaos/cafein"
31		"rengine"))
32		(defparameter tools
33		'("chaos/tools"
34		"regcheck" "regularize" "describe" "sort-tree" "module-tree"
35		"show" "set" "op-check" "compat"))
36		(defparameter eval
37		'("chaos/eval"
38		"eval-mod" "eval-ast" "eval-ast2" "chaos-top"))
39		(defparameter boot
40		'("chaos/boot"
41		"preproc" "prelude" "builtins"))
42		(defparameter tram
43		'("chaos/tram" "tram"))
44		(defparameter psup
45		'("chaos/psup" "psup"))
46		(defparameter thstuff
47		'("thstuff"
48		"parse-apply" "basics" "eval-match" "eval-apply" "cexec"))
49		(defparameter cafeobj
50		'("cafeobj"
51		"cafeobjvar" "creader" "trans-com" "trans-decl" "command-proc"
52		"command-top" "cafeobj-top"))
53
54		(defun load-cafeobj ()
55		(dolist (module (list top-files comlib primitives term-parser
56		e-match construct decafe cafein tools
57		eval boot tram psup thstuff cafeobj))
58		(let ((dir (car module))
59		(files (cdr module))
60		(path nil))
61		(dolist (file files)
62		;; (setq path (make-pathname :directory dir :name file :type "lisp"))
63		(setq path (concatenate 'string dir "/" file ".lisp"))
64		(load path)))))
65
66		;;; EOF

+72

-0

todo/2013/genCases.cafe less more

	0	-- the following two modules describe an algorithm
	1	-- for generating a finite set of patterns
	2	-- by expanding alternatives indicated by (_;_)
	3
	4	-- the formal parameter module for defining
	5	-- (1) predicate v_ that is to be checked, and
	6	-- (2) indicator information constructor ii
	7	mod* PREDtbc {
	8	-- values and their sequences
	9	[Val < ValSq]
	10	op _,_ : ValSq ValSq -> ValSq {assoc} .
	11	-- predicate to be checed
	12	pred v_ : ValSq .
	13	-- indicator information for analysis
	14	[IndInfo]
	15	op ii_ : ValSq -> IndInfo {constr} .
	16	** v_ and ii_ shoud have a same arity
	17	** as a sequence of 'Val's
	18	}
	19
	20	-- generating a finit set of patterns
	21	-- that cover all possible combinations
	22	-- of values in a value sequence
	23	mod GENcases (X :: PREDtbc) {
	24	-- sequences of values indicating
	25	-- all combinations indicated by
	26	-- alternative notations (_;_)
	27	[Val < VlSq]
	28	-- alternative sequence
	29	op _;_ : VlSq VlSq -> VlSq {assoc} .
	30	-- sequence of ValSeq or VlSeq
	31	[ValSq VlSq < SqSq]
	32	op empSS : -> SqSq .
	33	op _,_ : SqSq SqSq -> SqSq {assoc id: empSS} .
	34	-- SqSq enclosures and their trees
	35	[SqSqEn < SqSqTr]
	36	op [_] : SqSq -> SqSqEn .
	37	op _\|\|_ : SqSqTr SqSqTr -> SqSqTr .
	38
	39	-- generate all combinations of alternatives
	40	-- indicated by (_;_) into (_\|\|_)
	41	eq [(SS1:SqSq,(V:Val;VS:VlSq),SS2:SqSq)]
	42	= [(SS1,V,SS2)] \|\| [(SS1,VS,SS2)] .
	43
	44	-- indicators and their trees
	45	[Ind < IndTr]
	46	op $ : -> Ind .
	47	op _\|_ : IndTr IndTr -> IndTr .
	48	-- indicator constructor;
	49	-- [IndInfo] comes from (X :: PREDtbc)
	50	op i : Bool IndInfo -> Ind {constr} .
	51	-- make indicator (mi) using
	52	-- (v_ : ValSq -> Bool) and
	53	-- (ii_ : ValSq -> IndInfo)
	54	-- that come from (X :: PREDtbc)
	55	op mi_ : ValSq -> Ind .
	56	eq mi(VSQ:ValSq) = i(v(VSQ),ii(VSQ)) .
	57
	58	-- make make indicators (mmi):
	59	-- translating a tree of SqSq (SqSqTr)
	60	-- into a tree of indicators
	61	op mmi_ : SqSqTr -> IndTr .
	62	eq mmi(SST1:SqSqTr \|\| SST2:SqSqTr)
	63	= (mmi SST1) \| (mmi SST2) .
	64	-- if all _;_ in SqSq disappear
	65	-- then translate mmi to mi
	66	eq mmi[VSQ:ValSq] = mi(VSQ) .
	67
	68	-- making all indicators with "true" disappear
	69	eq i(true,II:IndInfo) \| IT:IndTr = IT .
	70	eq IT:IndTr \| i(true,II:IndInfo) = IT .
	71	}

+187

-0

todo/2013/qlock-lofPs.cafe less more

	0	** ===============================================================
	1	** ===== QLOCK Proof Score for a lockout free property ===========
	2	** ===============================================================
	3
	4	in qlock-sysProp.cafe
	5
	6	-- ===============================================================
	7	-- enhancing Peano Style Natural Numbers
	8	-- for defining necessary new state functions
	9	mod! PNATerr-a {pr(PNATerr)
	10	-- plus over Nat&Err
	11	op _+_ : Nat&Err Nat&Err -> Nat&Err {assoc comm} .
	12	-- associative and commutative _*_
	13	op _*_ : Nat&Err Nat&Err -> Nat&Err {assoc comm} .
	14	op _*_ : Nat Nat -> Nat {assoc comm} .
	15	eq 0 * Y:Nat = 0 .
	16	eq (s X:Nat) * Y:Nat = Y + (X * Y) .
	17	-- greater than Nat&Err
	18	op _>_ : Nat&Err Nat&Err -> Bool .
	19	}
	20
	21	mod* LABELerr {pr(LABEL)[Label < Label&Err]}
	22
	23	** ===============================================================
	24	-- enhanced elementary functions on states
	25	mod! STATEfuns-a {pr(STATEfuns + PNATerr-a + LABELerr)
	26	-- the depth of the first appearence of an aid in a queue
	27	op #daq : Qu Aid -> Nat&Err .
	28	op #daq-sub : Qu Aid -> Nat .
	29	ceq #daq(Q:Qu,A1:Aid) = #daq-sub(Q,A1) if not(#aq(Q,A1) = 0) .
	30	eq #daq-sub(A1:Aid & Q:Qu,A2:Aid) =
	31	if (A1 = A2) then 0 else s(#daq-sub(Q,A2)) fi .
	32	-- counter count of cs
	33	op #ccs : State -> Nat .
	34	eq #ccs(S:State) = if (#ls(S,cs) > 0) then 0 else (s 0) fi .
	35	-- decreasing Nat measure for the lockout freedom verification
	36	op #dms : State Aid -> Nat&Err .
	37	eq #dms(S:State,A:Aid) = ((s s s 0) * #daq(qu(S),A))
	38	+ #ls(S,rs) + #ccs(S) .
	39	-- the transition:
	40	-- (((b1 & q) $ (((lb [ b22 ] : ws) (lb [ b1 ] : cs)) as1)) ->
	41	-- (q $ ((lb [ b1 ] : rs) ((lb [ b22 ] : ws) as1)))
	42	-- increases (#ls(_,rs) + #ccs(_)) by (s s 0)
	43	-- decreases #daq(qu(_),b22)) by (s 0)
	44	-- so we need ((s s s 0) * (s 0) = (s s s 0))
	45	-- for proper decrease of #dms(_,b22)
	46
	47	-- label of an agent in a state
	48	op las : State Aid -> Label&Err .
	49	eq las((Q:Qu $ (lb[A:Aid]: L:Label) AS:Aobs),A) = L .
	50	}
	51
	52	-- load the module GENcases from genCases.cafe file
	53	in genCases.cafe
	54
	55	--> ==============================================================
	56	--> The following proof score proves that for any
	57	--> one-step transition:
	58	--> ((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS))
	59	--> -> SS)
	60	--> over the states, the predicate:
	61	--> (inv(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS))
	62	--> implies
	63	--> (#dms((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)),A1) >
	64	--> #dms(SS,A1)) and
	65	--> ((las(SS,A1) = cs) or (las(SS,A1) = ws)))
	66	--> holds.
	67	--> Note that inv is already proved to be an inductive invariant,
	68	--> and #dms is defined in the module STATEfuns-a as:
	69	--> eq #dms(S:State,A:Aid) = ((s s s 0) * #daq(qu(S),A))
	70	--> + #ls(S,rs) + #ccs(S) .
	71	-->
	72	--> Because #dms(_,_) is a natural number,
	73	--> it implies that for any state S and any aid A,
	74	--> if (lb[A]: ws) is a component of S,
	75	--> any sequence of transtions from S should finally
	76	--> leads to the state SS on which
	77	--> (1) (las(SS,A) = cs),
	78	--> or
	79	--> (2) (#dms(SS,A) = 0), that is
	80	--> (#daq(qu(SS),A)) = 0) and (#ls(SS,rs) = 0)
	81	--> and (#ccs(SS) = 0).
	82	--> It implies that a state of the form:
	83	--> (Q $ ((lb[A]: ws) AS))
	84	--> finally reaches to a state of the form:
	85	--> ((A & QQ) $ ((lb[A]: cs) AAS))
	86	--> no matter what sequence of transitions is taken.
	87	--> ==============================================================
	88
	89	-- qlock lockout freeness module:
	90	-- actual parameter for GENcases module
	91	mod QLOCKlof {pr(QLOCKsys + QLOCKprop + STATEfuns-a)
	92	-- val and ValSeq
	93	[Qu Aid Label Aobs State < Val < ValSq]
	94	op _,_ : ValSq ValSq -> ValSq {assoc} .
	95
	96	-- for indicating information for the fourth argument
	97	[IndInfo]
	98	op _->_!!_ : State State Bool -> IndInfo {constr} .
	99	op _!_ : Bool Bool -> Bool {constr assoc} .
	100	op nb_ : Nat&Err -> Bool .
	101
	102	-- predicate to be checked
	103	op v_ : ValSq -> Bool .
	104	eq v(Q:Qu,A1:Aid,A2:Aid,L2:Label,AS:Aobs,SS:State) =
	105	not((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)) =(*,1)=>+ SS
	106	suchThat
	107	not((inv(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS))
	108	implies
	109	(#dms((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)),A1) >
	110	#dms(SS,A1)) and
	111	((las(SS,A1) = cs) or (las(SS,A1) = ws)))
	112	== true)
	113
	114	{(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)) -> SS
	115	!!
	116	(inv(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS))
	117	implies
	118	(#dms((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)),A1) >
	119	#dms(SS,A1)))
	120	!
	121	inv(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS))
	122	!
	123	(#dms((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)),A1) >
	124	#dms(SS,A1))
	125	!
	126	nb(#dms((Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)),A1))
	127	!
	128	nb(#dms(SS,A1))
	129	}) .
	130
	131	-- for indicating information
	132	op ii_ : ValSq -> IndInfo .
	133	op ss_ : State -> IndInfo {constr} .
	134	eq ii(Q:Qu,A1:Aid,A2:Aid,L2:Label,AS:Aobs,SS:State)
	135	= ss(Q $ ((lb[A1]: ws)(lb[A2]: L2) AS)) .
	136	}
	137
	138	-- a module to generate and check all possible transitions
	139	mod! CKallCasesLof {ex(GENcases(QLOCKlof))
	140	-- constants declarations
	141	op q : -> Qu .
	142	op as : -> Aobs .
	143
	144	-- Aid constant literals
	145	[AidConLt < Aid]
	146	eq (B1:AidConLt = B2:AidConLt) = (B1 == B2) .
	147	ops b1 b21 b22 b3 : -> AidConLt .
	148	eq #aq(q,b21) = 0 .
	149	eq (#aq(q,b22) = 0) = false .
	150
	151	[AobsLt < Aobs]
	152	eq (AS1:AobsLt = AS2:AobsLt) = (AS1 == AS2) .
	153	ops as1 as2 : -> AobsLt .
	154	-- the following is complete case splitting
	155	-- because cj(mx,S:State) is an invariant
	156	eq #lss(as1,cs) = 0 .
	157	eq #lss(as2,cs) = (s 0) .
	158
	159	-- function for generating and checking all possible
	160	-- transitions defined by the module WT, TY, EX
	161	op gen&ck1 : State -> IndTr .
	162	eq gen&ck1(SS:State) =
	163	($ \| mmi[(empQ;(b1 & q)),
	164	(b1;(b21;b22)),
	165	(b1;(b21;b22);b3),
	166	(rs;ws;cs),
	167	(as1;as2),
	168	(SS)]) .
	169
	170	}
	171
	172	-- ===============================================================
	173	-- facts to be used
	174	mod! FACTtbu-a {pr(QLOCKprop + STATEfuns-a)
	175
	176	-- about #daq
	177	ceq #daq((Q:Qu & A1:Aid),A2:Aid) = #daq(Q,A2) if not(A1 = A2) .
	178	}
	179
	180	-- checking all possible cases
	181	open (CKallCasesLof + FACTtbu-a) .
	182	red gen&ck1(SS:State) .
	183	close
	184
	185	-- ==============================================================
	186	-- ==============================================================

+272

-0

todo/2013/qlock-sysProp.cafe less more

	0	** ===============================================================
	1	** ===== System and Proprerty Specification of QLOCK =============
	2	** ===============================================================
	3
	4	** ===============================================================
	5	** ============= QLOCK System Specification ======================
	6	** ===============================================================
	7
	8	-- three labels for indicating status of each agent
	9	mod! LABEL {
	10	-- label literals and labels
	11	[LabelLt < Label]
	12	-- rs: remainder section
	13	-- ws: waiting section
	14	-- cs: critical section
	15	ops rs ws cs : -> LabelLt {constr} .
	16	-- vars L1 L2 : LabelLt .
	17	eq (L1:LabelLt = L2:LabelLt) = (L1 == L2) .
	18	}
	19
	20	-- agent identifiers
	21	mod* AID {[Aid]}
	22
	23	-- ===============================================================
	24	-- queue (first in first out storage)
	25	mod! QUEUE (X :: TRIV) {
	26	-- elements and their queues, Elt comes from (X :: TRIV)
	27	[Elt.X < Qu]
	28	-- empty queue
	29	op empQ : -> Qu {constr} .
	30	-- assoicative queue constructors with id: empQ
	31	op (_&_) : Qu Qu -> Qu {constr assoc id: empQ} .
	32	-- equality _=_ over the sort Qu
	33	-- _=_ is defined for each sort in the built-in module EQL
	34	eq (empQ = (E:Elt & Q:Qu)) = false .
	35	ceq ((E1:Elt & Q1:Qu) = (E2:Elt & Q2:Qu))
	36	= ((E1 = E2) and (Q1 = Q2))
	37	if not((Q1 = empQ) and (Q2 = empQ)) .
	38	}
	39
	40	-- ===============================================================
	41	-- agent observer
	42	mod! AOB {pr(LABEL) pr(AID)
	43	[Aob]
	44	-- (lb[A:Aid]: L:Label) is a term of the sort Aobs
	45	-- (an observer) that indicates an agent A is in a label L
	46	-- i.e. (lb[A:Aid]: L:Label)
	47	op (lb[_]:_) : Aid Label -> Aob {constr} .
	48	}
	49	-- generic set
	50	mod! SET(X :: TRIV) {
	51	[Elt.X < Set]
	52	-- empty set
	53	op empty : -> Set {constr} .
	54	-- assicative and commutative set constructor with identity empty
	55	op (_ _) : Set Set -> Set {constr assoc comm id: empty} .
	56	-- (_ _) is idempotent with respect to the sort Elt
	57	eq E:Elt E = E .
	58	}
	59	-- queue of Aid
	60	mod! AID-QUEUE {pr(QUEUE(AID{sort Elt -> Aid}))}
	61	-- a state is defined as a pair of queue of Aid and a set of Aob
	62	mod! STATE{
	63	pr(AID-QUEUE)
	64	pr(SET(AOB{sort Elt -> Aob})*{sort Set -> Aobs})
	65	-- a state is a pair of Qu and Aobs
	66	[State]
	67	op _$_ : Qu Aobs -> State {constr} .
	68	}
	69
	70	-- ===============================================================
	71	-- wt: want transition
	72	mod! WT {pr(STATE)
	73	trans[wt]:
	74	(Q:Qu $ ((lb[A:Aid]: rs) AS:Aobs))
	75	=> ((Q & A) $ ((lb[A ]: ws) AS)) .
	76	}
	77	-- ty: try transition
	78	mod! TY {pr(STATE)
	79	trans[ty]:
	80	((A:Aid & Q:Qu) $ ((lb[A]: ws) AS:Aobs))
	81	=> ((A & Q) $ ((lb[A]: cs) AS)) .
	82	}
	83	-- ex: exit transition
	84	mod! EX {pr(STATE)
	85	trans[ex]:
	86	((A1:Aid & Q:Qu) $ ((lb[A2:Aid]: cs) AS:Aobs))
	87	=> (Q $ ((lb[A2 ]: rs) AS)) .
	88	}
	89
	90	-- ===============================================================
	91	-- system specification of QLOCK
	92	mod! QLOCKsys{pr(WT + TY + EX)}
	93
	94	** ===============================================================
	95	** ================ Property Specification =======================
	96	** ===============================================================
	97
	98	-- ===============================================================
	99	-- for defining state functions and predicates we need
	100	-- Peano Style Natural Numbers with _+_ and _>_
	101	mod! PNAT {
	102	[Nat]
	103	op 0 : -> Nat {constr} .
	104	op s_ : Nat -> Nat {constr} .
	105	-- equality over the natural numbers
	106	eq (0 = s(Y:Nat)) = false .
	107	eq (s(X:Nat) = s(Y:Nat)) = (X = Y) .
	108	eq (s(X:Nat) = X) = false .
	109	-- associative and commutative _+_
	110	[Nat]
	111	op _+_ : Nat Nat -> Nat {assoc comm} .
	112	eq 0 + Y:Nat = Y .
	113	eq (s X:Nat) + Y:Nat = s(X + Y) .
	114	-- strict greater than
	115	op _>_ : Nat Nat -> Bool .
	116	eq (s X:Nat) > 0 = true .
	117	eq 0 > (s Y:Nat) = false .
	118	eq (s X:Nat) > (s Y:Nat) = X > Y .
	119	eq (s X:Nat) > X = true .
	120	eq X:Nat > (s X) = false .
	121	eq X:Nat > X = false .
	122	}
	123
	124	-- for defining tl(empQ)/hd(empQ) and #aq(tl Q:Qu)
	125	mod* PNATerr {pr(PNAT) [Nat < Nat&Err]}
	126	mod* AID-QUEUEerr {pr(AID-QUEUE)
	127	-- error elements
	128	[Aid < Aid&Err]
	129	-- head
	130	op hd_ : Qu -> Aid&Err .
	131	eq hd(E:Aid & Q:Qu) = E .
	132	-- hd(empQ):Aid&Err indicates an error element
	133	-- and no equations for it; an error handling method
	134	-- error queues
	135	[Qu < Qu&Err]
	136	-- tail
	137	op tl_ : Qu -> Qu&Err .
	138	eq tl(E:Aid & Q:Qu) = Q .
	139	-- tl(empQ):Qu&Err indicates an error queue
	140	-- and no equations for it; an error handling method
	141	}
	142
	143	** ===============================================================
	144	-- elementary functions on states
	145	mod! STATEfuns {pr(STATE + PNATerr + AID-QUEUEerr)
	146	-- the queue in a state
	147	op qu : State -> Qu .
	148	eq qu(Q:Qu $ AS:Aobs) = Q .
	149	-- the agent observations in a state
	150	op aos : State -> Aobs .
	151	eq aos(Q:Qu $ AS:Aobs) = AS .
	152	-- length of Aobs
	153	op #laos : Aobs -> Nat .
	154	eq #laos(empty) = 0 .
	155	eq #laos(A:Aob AS:Aobs) = (s 0) + #laos(AS) .
	156	-- the number of a label in a state
	157	op #ls : State Label -> Nat .
	158	-- #ls's subordinate operator
	159	op #lss : Aobs Label -> Nat .
	160	eq #lss(empty,L:Label) = 0 .
	161	eq #lss(((lb[A:Aid]: L1:Label) AS:Aobs),L2:Label) =
	162	if (L1 = L2) then (s 0) + #lss(AS,L2) else #lss(AS,L2) fi .
	163	eq #ls(S:State,L:Label) = #lss(aos(S),L) .
	164	-- the number of an aid in a state
	165	op #as : State Aid -> Nat .
	166	-- #as's sub operator
	167	op #ass : Aobs Aid -> Nat .
	168	eq #ass(empty,A:Aid) = 0 .
	169	eq #ass(((lb[A1:Aid]: L:Label) AS:Aobs),A2:Aid) =
	170	if (A1 = A2) then (s 0) + #ass(AS,A2) else #ass(AS,A2) fi .
	171	eq #as(S:State,A:Aid) = #ass(aos(S),A) .
	172	-- the number of an aid in a queue
	173	-- Qu&Err and Nat&Err are used for handing #aq(tl Q:Qu)
	174	op #aq : Qu&Err Aid -> Nat&Err .
	175	op #aq : Qu Aid -> Nat .
	176	eq #aq(empQ,A:Aid) = 0 .
	177	eq #aq(A1:Aid & Q:Qu,A2:Aid) =
	178	if (A1 = A2) then (s 0) + #aq(Q,A2) else #aq(Q,A2) fi .
	179	}
	180
	181	-- ===============================================================
	182	-- names of predicates on states and conjunction of the predicates
	183	mod! PNAMEcj {pr(STATE)
	184	-- names of predicates on States and sequences of them
	185	[Pname < PnameSeq]
	186	op (_ _) : PnameSeq PnameSeq -> PnameSeq {assoc} .
	187	-- conjunction of predicates indicated in PnameSeq
	188	op cj : PnameSeq State -> Bool .
	189	eq cj(PN:Pname PNS:PnameSeq,S:State)
	190	= cj(PN,S) and cj(PNS,S) .
	191	}
	192
	193	-- ===============================================================
	194	-- predicates on states for well formed states and intitial states
	195	mod! STATEpred-init {pr(STATEfuns + PNAMEcj)
	196	-- at least one agent in a state
	197	op aoa : -> Pname .
	198	eq[aoa]: cj(aoa,S:State) = (#laos(aos(S)) > 0) .
	199	-- no duplication of an Aid in a state
	200	op 1a : -> Pname .
	201	-- sub for 1a
	202	op 1as : Aobs -> Bool .
	203	eq 1as(empty) = true .
	204	eq 1as((lb[A:Aid]: L:Label) AS:Aobs) =
	205	(#ass(AS,A) = 0) and 1as(AS) .
	206	eq[1a]: cj(1a,S:State) = 1as(aos(S)) .
	207	-- well formed states
	208	op wfs : -> Pname .
	209	eq[wfs]: wfs = aoa 1a .
	210	-- the queue is empty
	211	op qe : -> Pname .
	212	eq[qe]: cj(qe,S:State) = (qu(S) = empQ) .
	213	-- any Aid is in rs status, i.e. no ws, no cs
	214	op allRs : -> Pname .
	215	eq[allRs]: cj(allRs,S:State) = (#ls(S,ws)= 0) and (#ls(S,cs)= 0) .
	216	}
	217
	218	-- ===============================================================
	219	-- an initial state predicate
	220	mod! INIT {pr(STATEpred-init)
	221	op init : -> PnameSeq .
	222	eq init = wfs qe allRs .
	223	-- initial state predicate
	224	pred init : State .
	225	eq init(S:State) = cj(init,S) .
	226	}
	227
	228	-- ===============================================================
	229	-- predicates on states for an inductive invariant predicate
	230	mod! STATEpred-inv {pr(STATEpred-init + AID-QUEUEerr)
	231	-- mutual exclusion property: at most one agent is with cs
	232	-- this is the goal predicate
	233	op mx : -> Pname .
	234	eq[mx]: cj(mx,S:State) = ((#ls(S,cs) = 0) or (#ls(S,cs) = (s 0))) .
	235	-- several fragment predicates for an inductive invariant
	236	ops qep rs ws cs : -> Pname .
	237	-- if queue is empty
	238	eq[qep]: cj(qep,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs)))
	239	= ((Q = empQ) implies
	240	(#lss(((lb[A]: L) AS),cs) = 0)) .
	241	-- if agent is in rs
	242	eq[:m-and rs]: cj(rs,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs)))
	243	= ((L = rs) implies (#aq(Q,A) = 0)) .
	244	-- if agent is in ws
	245	eq[:m-and ws]: cj(ws,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs)))
	246	= ((L = ws) implies
	247	((#aq(Q,A) = (s 0)) and
	248	((A = hd(Q)) implies (#lss(AS,cs) = 0)))) .
	249	-- if agent is in cs
	250	eq[:m-and cs]: cj(cs,(Q:Qu $ ((lb[A:Aid]: L:Label) AS:Aobs)))
	251	= ((L = cs) implies ((A = hd(Q)) and
	252	(#aq(tl(Q),A) = 0)and
	253	(#lss(AS,cs) = 0))) .
	254	}
	255
	256	-- ===============================================================
	257	-- an inductive invariant predicate
	258	mod! INV {pr(STATEpred-inv)
	259	op inv : -> PnameSeq .
	260	eq inv = wfs mx qep rs ws cs .
	261	pred inv : State .
	262	eq inv(S:State) = cj(inv,S) .
	263	}
	264
	265	-- ===============================================================
	266	-- property specification of QLOCK
	267	mod! QLOCKprop{pr(INIT + INV)}
	268
	269	-- ===============================================================
	270	-- ===============================================================
	271

-1

version.lisp less more

8	8	(eval-when (:execute :load-toplevel :compile-toplevel)
9	9	(setq cafeobj-version-major "1.4")
10	10	(setq cafeobj-version-memo (format nil "~a" "PigNose0.99"))
11		(setq patch-level (format nil "~a" "alpha-1"))
	11	(setq patch-level (format nil "~a" "a2"))
12	12	(if (not (equal "" cafeobj-version-memo))
13	13	(if (not (equal "" patch-level))
14	14	(setq cafeobj-version-minor