|
|
|
|
|
|
| New in Version 1.1
|
|
| This page lists all the major changes and new features of the LWB 1.1 compared to the previous version. | ||
|
|  | ||
|
|
Main Changes | |||
 | now versions for Linux and Macintosh | |||
| new Solaris GUI | |||
| new interrupt handling, limiting of computation time and string manipulation functions | |||
| new, fast BDD-based decision procedure, computation of truth tables and the Quine-McCluskey algorithm for the classical propositional calculus cpc | |||
| faster decision procedure for pltl (linear temporal logic) | |||
| considerably improved information messages and progress indication in all modules | |||
| more than fifty new functions | |||
| additional tests, thus more guarantee for correct results | |||
| better interrupt mechanism which frees more memory and is more stable, i.e. the LWB can be interrupted at any time | |||
|
| | ||
|
| The following is a more detailed list of changes made for the LWB 1.1, split into subgroups. | |||
|
| | ||
|
|
Graphical User Interfaces | |||
| This part contains the changes and additions that were made to all graphical user interfaces. | ||||
 Text Regions
| regions containing simple text, which is not parsed or executed can now be defined | |||
| Font Selection
| font selection for input, output, text and information regions | |||
| Pretty Mode
| support for the display of connectives and special symbols using special character codes in a font, translates operators and greek symbols to special characters. | |||
| Save/Load Configurations
| configurations can now be saved to and loaded from arbitrary files, which allows multiple configurations | |||
|
|
XLWB | |||
| Only the things that are unique to the XLWB are listed in this part. | ||||
| Separator
| a separator line can be inserted for visual separation of parts of a session | |||
| Prompt Handling
| has been improved | |||
|
|
MacLWB | |||
| The MacLWB is completely new, thus everything could be noted as being new. To avoid too many repeatings, only things that are in addition to the XLWB user interface are listed here. | ||||
| Printing
| single regions, whole sessions and the information window can directly be printed | |||
| Icons
| icons for LWB session files and LWB value files are available, these file can be loaded with a double click | |||
| URL SAES
| the LWB uses the URL Standard Apple Event Suite to communicate to all standard macintosh web browsers used for the help system | |||
| Installation
| easy to use installation package | |||
| Documentation
| complete documentation of all Macintosh specific functions, menus and keystrokes | |||
| LWB Settings
| all LWB settings can be configured using the graphical user interface | |||
| Indentation
| new lines started within a region are automatically indented | |||
| Selection
| text can easily be selected using the Shift and Cursor keys | |||
| Show/Hide
| show and hide of individual regions, per keyboard sequence or mouse click | |||
| Keystrokes
| additional keyboard sequences are provided for direct movement to special places of a region | |||
| Interrupts
| comfortable interrupt system, allowing to interrupt any computation | |||
|
| | ||
|
|
ProofWish | |||
| Font
| The font displayed can now be freely selected | |||
| Pure Tcl/Tk
| the ProofWish tool now uses pure Tcl/Tk only, itcl is no more necessary | |||
| Tcl/Tk 8.0
| now requires Tcl/Tk 8.0 | |||
| Bugs
| some bugs were removed | |||
| Mac Version
| the ProofWish tool has been ported to the Macintosh, along with a connection to the MacLWB | |||
| Documentation
| there is now a complete documentation of all the functions of the ProofWish toll | |||
|
| | ||
|
|
User Module | |||
get
| get configuration (previously obtained with set()), now
individual configuration values can be checked
| |||
index
| get the index of a symbol or an indexed connective symbol | |||
less
| compare two expressions and get their ordering | |||
limitstart
| start limiting of computation time and set the time for it. With this feature, the computation time can be limited for subsequent commands. When the time has passed, an error is raised (which can be caught, using the LWB programming language). | |||
limitstop
| stop limiting of computation time, computation is no more limited | |||
pretty
| print an expression using the pretty font, i.e. displaying connectives and other symbols with their correct signs of the font | |||
randomint
| compute and return a random integer value | |||
randomize
| initialize the random number generator, i.e. set the random seed | |||
read
| this function is now a standard function and thus requires brackets around its argument | |||
save
| this function is now a standard function and thus requires brackets around its argument | |||
sort
| sort a list of expressions | |||
strconcat
| concatenate two or more strings to a new string | |||
strindex
| determine the occurrence of a string in another string | |||
string
| convert a symbol into a string | |||
strleft
| return the head characters of a string | |||
strlen
| compute the length of a string | |||
strmid
| return a substring of a string | |||
strright
| return the tail characters of a string | |||
timestart
| this function is now a standard function and thus requires brackets around its argument | |||
timestop
| this function is now a standard function and thus requires brackets around its argument | |||
union
| create the union of lists or arrays | |||
|
| | ||
|
|
CPC Module | |||
| the information messages and progress indications are improved in all functions | ||||
bddsat
| determine if a formula is satisfiable, using BDDs | |||
convert
| the function is slightly improved | |||
model
| compute a model of a formula | |||
qmc
| apply the Quine-McCluskey algorithm an a formula to obtain a 'minimal' formula in disjunctive normal form | |||
simplify
| improvements in the algorithm for better simplification in some special cases | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
truthtable
| compute and display the truthtable of a formula | |||
value
| determine the value of a formula in a special model | |||
vars
| some new options added | |||
|
| | ||
|
|
IPC Module | |||
| the information messages and progress indications are improved in all functions | ||||
convert
| the function is slightly improved | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
K Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
KT Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
S4 Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
S5 Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
G Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
Kn Module | |||
| the information messages and progress indications are improved in all functions | ||||
boxnr
| add a box connective with an index | |||
dianr
| add a diamond connective with an index | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
wisemen
| theory more closely reflects general understanding | |||
|
| | ||
|
|
KTn Module | |||
| the information messages and progress indications are improved in all functions | ||||
boxnr
| add a box connective with an index | |||
dianr
| add a diamond connective with an index | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
wisemen
| theory more closely reflects general understanding | |||
|
| | ||
|
|
TK Module | |||
| the information messages and progress indications are improved in all functions | ||||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
PLTL Module | |||
display
| display function for timing diagrams | |||
model
| search for a model of a function, yields a lineal model if formula is satisfiable | |||
provable
| now functions correctly and is faster, based on tableau-graph expansion and SCC-analysis | |||
W operator
| the weak until operator, introduced for efficiency reasons, replaces
the still available function
wu
| |||
|
| | ||
|
|
LL Module | |||
| No changes were made to this module. | ||||
|
| | ||
|
|
AEL Module | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
CIRC Module | |||
| the information messages and progress indications are improved in all functions | ||||
arrange
| arrange a formula or theory | |||
convert
| convert connectives | |||
remove
| remove superfluous connectives and subformulas of a formula or theory | |||
simplify
| simplify a formula | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
CWA Module | |||
| the information messages and progress indications are improved in all functions | ||||
arrange
| arrange a formula or theory | |||
consistent
| now works correctly | |||
convert
| convert connectives | |||
remove
| remove superfluous connectives and subformulas of a formula or theory | |||
simplify
| simplify a formula | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
vars
| some new options added | |||
|
| | ||
|
|
Default Module | |||
| the information messages and progress indications are improved in all functions | ||||
arrange
| arrange a formula or theory | |||
consistent
| now works correctly | |||
convert
| convert connectives | |||
remove
| remove superfluous connectives and subformulas of a formula or theory | |||
simplify
| simplify a formula | |||
subfmls
| compute the list of all subformulas of a formula or theory | |||
symmetric
| construct a default theory with many extensions | |||
vars
| some new options added | |||
|
| ||||
| 
| 
| ||
|
| lwb@iam.unibe.ch | LWB 1.1 February 22, 2002 |