packages feed

cpsa 2.3.1 → 2.3.2

raw patch · 12 files changed

+129/−58 lines, 12 files

Files

ChangeLog view
@@ -1,3 +1,22 @@+2014-01-07  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as version 2.3.2++2013-12-27  John D. Ramsdell  <ramsdell@mitre.org>++	* src/prover9.pl: Reverted to work with strings as tags fixing a+	bug introduced in version 2.3.1.++2013-12-14  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Extra-Source-Files):  Sorted the files.++2013-10-15  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as version 2.3.1++	* src/unsorted.pl: Added a missing occurs check and substitution.+ 2013-10-11  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Cohort.hs (prioritizeVertices): Reversed the sort
NEWS view
@@ -1,5 +1,11 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.3.2++** Bug fixed in prover9+   A bug was introduced in 2.3.1 that caused it to fail when the input+   contains a tag.+ * Changes in version 2.3.1  ** Bug in priority ordering fixed.
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.3.1+Version:		2.3.2 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -64,18 +64,25 @@   src/cpsaextras/Main.scala src/cpsaextras/Pretty.scala   src/cpsaextras/Printer.scala src/cpsaextras/SExpr.scala   tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall-  tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst-  tst/completeness-test.scm tst/completeness-test.tst tst/crushing.tst-  tst/crushing.tst tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm+  tst/cpsashapesall +  tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm+  tst/completeness-test.tst tst/crushing.tst tst/crushing.tst+  tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm   tst/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst-  tst/deorig_contract.scm tst/deorig_contract.tst-  tst/deorig_simple.scm tst/deorig_simple.tst-  tst/ds-short.lisp tst/deorig_mesg.scm tst/deorig_mesg.tst tst/dy.lsp-  tst/dy.tst tst/encsig.scm tst/encsig.tst tst/epmo_acctnum.lisp-  tst/epmo.scm tst/epmo.tst tst/ffgg.scm-  tst/ffgg.tst tst/fragile_pruning.scm tst/fragile_pruning.tst+  tst/deorig_contract.scm tst/deorig_contract.tst tst/deorig_mesg.scm+  tst/deorig_mesg.tst tst/deorig_simple.scm tst/deorig_simple.tst+  tst/DH_hack.scm tst/DH_hack.tst tst/ds-short.lisp tst/dy.lsp+  tst/dy.tst tst/encsig.scm tst/encsig.tst+  tst/epmo_acctnum-key-hash.scm tst/epmo_acctnum-key-hash.tst+  tst/epmo_acctnum.lisp tst/epmo-hash.scm tst/epmo-hash.tst+  tst/epmo-key-hash.scm tst/epmo-key-hash.tst tst/epmo.scm+  tst/epmo.tst tst/ffgg.scm tst/ffgg.tst tst/fragile_pruning.scm+  tst/fragile_pruning.tst tst/hashtest-key-hash.scm+  tst/hashtest-key-hash.tst tst/hashtest.scm tst/hashtest.tst+  tst/incompleteness_example.scm tst/incompleteness_example.tst   tst/isoreject.scm tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst   tst/kelly64.lisp tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst+  tst/mass2.lsp tst/mass2.tst tst/mass.lsp tst/mass.tst   tst/missing_contraction.scm tst/missing_contraction.tst   tst/neuman-stubblebine-alt.lisp tst/neuman-stubblebine-reauth.lisp   tst/neuman-stubblebine-reauth.lsp tst/neuman-stubblebine-reauth.tst@@ -84,31 +91,25 @@   tst/nonaug-prune.tst tst/non_transforming.scm   tst/non_transforming.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4cm1.lsp   tst/nsl4cm1.tst tst/nsl4.lisp tst/nsl4resp2.lisp tst/nsl5i.lisp-  tst/nsl5.lisp tst/nslsk.scm tst/nslsk.tst tst/ns.scm tst/ns.tst-  tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst tst/pruning1.scm-  tst/pruning1.tst tst/sigenc.scm tst/sigenc.tst-  tst/sorted_epmo_acctnum.scm tst/sorted_epmo_acctnum.tst-  tst/targetterms2.scm tst/targetterms2.tst tst/targetterms6.scm-  tst/targetterms6.tst tst/targetterms8.scm tst/targetterms8.tst-  tst/tnsl5.lisp tst/uncarried_keys.scm tst/uncarried_keys.tst-  tst/uo.scm tst/uo.tst tst/updatetst tst/weird.scm tst/weird.tst-  tst/wide-mouth-frog.lsp tst/wide-mouth-frog.tst-  tst/wide-mouth-frog-scyther.lsp tst/wide-mouth-frog-scyther.tst+  tst/nsl5.lisp tst/ns-l.scm tst/nslsk.scm tst/nslsk.tst tst/ns-l.tst+  tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst+  tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst tst/pkinit.scm+  tst/pkinit.tst tst/preprocess.scm tst/preprocess.tst tst/print.scm+  tst/print.tst tst/pruning1.scm tst/pruning1.tst tst/sigenc.scm+  tst/sigenc.tst tst/sorted_epmo_acctnum.scm+  tst/sorted_epmo_acctnum.tst tst/targetterms2.scm+  tst/targetterms2.tst tst/targetterms6.scm tst/targetterms6.tst+  tst/targetterms8.scm tst/targetterms8.tst tst/timestamping.scm+  tst/timestamping.tst tst/tnsl5.lisp tst/uncarried_keys.scm+  tst/uncarried_keys.tst tst/uo.scm tst/uo.tst tst/updatetst+  tst/wang-hash.scm tst/wang-hash.tst tst/wang-key-hash.scm+  tst/wang-key-hash.tst tst/wang.lisp tst/weird.scm tst/weird.tst+  tst/wide-mouth-frog.lsp tst/wide-mouth-frog-scyther.lsp+  tst/wide-mouth-frog-scyther.tst tst/wide-mouth-frog.tst   tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm   tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm   tst/woolam.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst-  tst/yahalom.scm tst/yahalom.tst tst/epmo_acctnum-key-hash.scm-  tst/epmo_acctnum-key-hash.tst tst/epmo-key-hash.scm-  tst/epmo-key-hash.tst tst/wang.lisp tst/pkinit.scm tst/pkinit.tst-  tst/print.scm tst/print.tst tst/epmo-hash.scm tst/epmo-hash.tst-  tst/hashtest-key-hash.scm tst/hashtest-key-hash.tst tst/hashtest.scm-  tst/hashtest.tst tst/wang-key-hash.scm tst/wang-key-hash.tst-  tst/wang-hash.scm tst/wang-hash.tst tst/mass.lsp tst/mass.tst-  tst/mass2.lsp tst/mass2.tst tst/DH_hack.scm tst/DH_hack.tst-  tst/timestamping.scm tst/timestamping.tst tst/ns-l.scm tst/ns-l.tst-  tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst-  tst/preprocess.scm tst/preprocess.tst tst/incompleteness_example.scm-  tst/incompleteness_example.tst+  tst/yahalom.scm tst/yahalom.tst  -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry.
doc/cpsadesign.pdf view

binary file changed (275306 → 275294 bytes)

doc/cpsaintroslides.pdf view

binary file changed (93151 → 93144 bytes)

doc/cpsaoverview.pdf view

binary file changed (129004 → 128994 bytes)

doc/cpsaprimer.pdf view

binary file changed (273718 → 273706 bytes)

doc/cpsaspec.pdf view

binary file changed (411100 → 410979 bytes)

doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.3.1}+\newcommand{\version}{2.3.2} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/DiffieHellman/Algebra.hs view
@@ -869,7 +869,9 @@ idSubst subst (F Exp [t0, G t1]) =     case idSubst subst t0 of    -- (exp (exp g x) y) = (exp g (mul x y))       F Exp [t0', G t1'] ->-          idSubst subst (F Exp [t0', G $ mul t1' t1])+          case mul t1' $ groupSubst subst t1 of+            t2 | M.null t2 -> t0'+               | otherwise -> F Exp [t0', G t2]       t -> expSubst subst t t1 idSubst subst (F s u) =     F s (map (idSubst subst) u)@@ -1087,7 +1089,9 @@       F Exp [t0, G t1] ->           case substChase subst t0 of             F Exp [t0', G t1'] ->-                substChase subst (F Exp [t0', G $ mul t1' t1])+              case mul t1' $ groupChase subst t1 of+                t2 | M.null t2 -> t0'+                   | otherwise -> F Exp [t0', G t2]             t -> expChase subst t t1       F s u ->           F s (map (substChase subst) u)
src/prover9.pl view
@@ -203,11 +203,16 @@ 	load_term(Term, Internal), 	term_pp(Internal, Pretty). -%% Load a term using CPSA's parsing rules for terms.+%% Load a term using CPSA's parsing rules for terms.  Also, convert+%% variables into uppercase atoms, and constants into lowercase atoms.  load_term(Term, Internal) :- 	atom(Term),-	load_atom(Term, Internal).+	upcase_symbol(Term, Internal).+load_term(Term, Internal) :-+	string(Term),+	string_to_atom(Term, Atom),+	downcase_symbol(Atom, Internal). load_term(Term, Term) :- 	integer(Term), 	Term >= 0.@@ -228,33 +233,28 @@ 	atom(Term), 	load_terms(Terms, Internals). -%% Convert variables into uppercase atoms, and constants into-%% lowercase atoms.+upcase_symbol(Atom, Symbol) :-+	atom_chars(Atom, Chars),+	upcase_parts(Chars, Parts),+	atom_chars(Symbol, Parts). -load_atom('""', []) :- % The name for a listener is the null constant.-        !.-load_atom(Atom, Symbol) :--        atom_chars(Atom, Chars),-	parts(Chars, Parts),+upcase_parts([First|Rest], [Lead|Tail]) :-+	upcase_atom(First, Lead),+	symbol_parts(Rest, Tail).++downcase_symbol(Atom, Symbol) :-+	atom_chars(Atom, Chars),+	downcase_parts(Chars, Parts), 	atom_chars(Symbol, Parts). -parts(['"'|Chars], Parts) :--        !,-        downcase_parts(Chars, Parts).-parts(Chars, Parts) :--        upcase_parts(Chars, Parts).+%% The null constant is used for the name of the listener role. +downcase_parts([], ['[', ']']). downcase_parts([First|Rest], [Lead|Tail]) :- 	downcase_atom(First, Lead), 	symbol_parts(Rest, Tail). -upcase_parts([First|Rest], [Lead|Tail]) :--	upcase_atom(First, Lead),-	symbol_parts(Rest, Tail).- symbol_parts([], []).-symbol_parts(['"'], []) :--        !. symbol_parts(['-'|Rest], ['_'|Tail]) :- 	!, 	symbol_parts(Rest, Tail).
src/unsorted.pl view
@@ -8,7 +8,8 @@ %% modify it under the terms of the BSD License as published by the %% University of California. -:- module(unsorted, [to_unsorted/3, from_unsorted/3, unify/3, unify/4]).+:- module(unsorted, [to_unsorted/3, from_unsorted/3, +                     unify/3, unify/4, subst/3]).  :- use_module(cpsa). @@ -165,9 +166,21 @@     lookup(Key, Map, Result),     !,     Result = Value.	   % Fails when key is mapped to another value-% Extend Map when Key is not mapped-extend_map(Key, Value, Map, [(Key, Value)|Map]).+% Extend Map when Key is not mapped as long as var does occur in term+extend_map(Key, Value, Map, [(Key, Value)|Map]) :-+    \+occurs(Key, Value). +occurs(Var, Var).+occurs(Var, Term) :-+    Term =.. [_|Terms],+    occurs_list(Var, Terms).+    +occurs_list(Var, [Term|_]) :-+    occurs(Var, Term),+    !.+occurs_list(Var, [_|Terms]) :-+    occurs_list(Var, Terms).+ %% Unification of unsorted terms given the equation invk(invk(k)) = k.  %% unify(+Term0, +Term1, -Subst).@@ -250,3 +263,31 @@ unify_list([Term0|Terms0], [Term1|Terms1], InSubst, OutSubst) :-     unify(Term0, Term1, InSubst, Subst),     unify_list(Terms0, Terms1, Subst, OutSubst).++%% Substition++%% subst(+InTerm, +Subst, -OutTerm).++subst(InTerm, Subst, OutTerm) :-+    chase(InTerm, Subst, Term),+    subst_aux(Term, Subst, OutTerm).++subst_aux(Term, _, Term) :-+    atom(Term),+    !.+subst_aux(Term, _, Term) :-+    string(Term),+    !.+% Apply equation+subst_aux(invk(InTerm), Subst, OutTerm) :-+    subst(InTerm, Subst, invk(OutTerm)),+    !.+subst_aux(InTerm, Subst, OutTerm) :-+    InTerm =.. [Fun|InTerms],+    subst_list(InTerms, Subst, OutTerms),+    OutTerm =.. [Fun|OutTerms].++subst_list([], _, []).+subst_list([InTerm|InTerms], Subst, [OutTerm|OutTerms]) :-+    subst(InTerm, Subst, OutTerm),+    subst_list(InTerms, Subst, OutTerms).