How to use the old APTS system for SQ+ to C or Low SETL to C translation (11/26/99, revised 12/5/00 for SB, Annie Liu) there are five steps: steps 1-2: setting up for running setl2, as you've done. steps 3-4: setting up for running apts. step 5: running apts on examples. 1. set path to find setl2: set path=(/home/facfs1/liu/tools/setl2-2.3/bin $path) 2. set where you want to put your setl2 library: setenv SETL2_LIB /setl.lib and copy /home/facfs1/liu/tools/aptsOld/setl.lib into your setl2 library: cp /home/facfs1/liu/tools/aptsOld/setl.lib /setl.lib 3. set where you want to put your apts library: setenv APTS_LIB /apts.lib and copy /home/facfs1/liu/tools/aptsOld/apts.lib into your apts library: cp /home/facfs1/liu/tools/aptsOld/apts.lib /apts.lib 4. go to where you want to run examples, and copy the files below: cp /home/facfs1/liu/tools/aptsOld/src/{axiom.ax,c.c,dec.h,read.h,timer.h} . 5. get an example from /home/facfs1/liu/tools/aptsOld/src/ and run: there are two kinds of examples: (1) SQ+ specifications and their translation into C (2) Low SETL programs (with type annotations) and their translation into C for an example of (1), say graph reachability: copy source file and data file: cp /home/facfs1/liu/tools/aptsOld/src/{reach.src,reach1000.in} . start apts and run SQ+ to C translator: stlx apts >: loadcm squb; -- load translator executables >: sq2x (reach, reach1000); -- translate reach example and input -- whenever it pauses, type in a "continue;" to continue; -- when it asks to supply an identifier for something, do so; -- whenever it asks for a type for something, type in "int"; -- finally, it says "The final C program appears just below." -- but the C code is actually put in file "testc.src", -- and the translated input is put in file "reach1000.out". >: stop; -- exit cc c.c -- compile the generated C code a.out < reach1000.out -- run on given input for an example of (2), say graph reachability: copy source file and data file: cp /home/facfs1/liu/tools/aptsOld/src/{reachbnf.src,reach1000.in} . start apts and run Low SETL to C translator: stlx apts >: loadcm squb; -- load translator executables >: setlx (reachbnf, reach1000); -- translate reach example and input -- what you need to do is the same as for SQ+ to C translation, except -- that you are not asked to supply identifiers; the rest are same too. >: stop; -- exit cc c.c -- compile the generated C code a.out < reach1000.out -- run on given input to check whether the answer is correct, you can run the Low SETL code: cp /home/facfs1/liu/tools/aptsOld/src/reachbnf.stl . -- same as reachbnf.src, but with type annotations in comments stlc -o2 reachbnf.stl stlx reachbnf < reach1000.in some additional examples: for SQ+ to C translation: >:sq2x(cycle,cycle1000); -- cycle testing >:sq2x(aclose,aclose1000); -- attribute closure >:sq2x(live,livesmall); -- dead-code analysis for Low SETL to C translation: >:setlx(cyclebnf,cycle1000); -- cycle testing >:setlx(centbnf,cent1000); -- tree center >:setlx(orbitbnf,orbit); -- largest orbit >:setlx(maxindbnf,maxind1000); -- maximal independent set >:setlx(topsortbnf,top1000); -- topological sort >:setlx(aclosebnf,aclose1000); -- attribute closure >:setlx(dijkstrabnf,dijk1000); -- dijkstra's shortest path >:setlx(floydbnf,dijk1000); -- shortest path tree, seems like >:setlx(kruskal,krusk); -- kruskal's minimum spanning tree >:setlx(short, short1); -- shortest path tree again, seems like for the last three examples, the generated C code did not compile.