version 0.93 (1 October 2003)
This applet allows user to draw two-dimensional modal frames and check whether they satisfy commutativity and Church-Rosser properties, i.e. whether they are frames for product logics.
Select `New point' in the popup menu to create a starting point and then from the popup menu of a point create outgoing arrows (blue ones denote accessibility relation of the horizontal modality and red ones for the vertical modality).
Point and arrows can be dragged over the field to make the layout better. Two distinct points can be merged into one by dropping one onto another (black square surrounding the point appears to indicate this operation). And `Align arrow' in the arrow popup menu puts the control point of the arrow on half-way between the endpoints (making the arrow straight).
Points and arrows can be removed using their popup menus (`Remove point' and `Remove arrow', respectively).
Menus `H-modality' and `V-modality' contain options for horizontal and vertical modality types:
For all modalities (except the basic one) there are weakly connected versions as well -- their names are ending with .3. In the case of transitive or transitive-reflexive modality the actual accessibility relation is the transitive (and transitive-reflexive, respectively) closure of the displayed relation. The program automatically checks whether one-dimensional components satisfy conditions for the selected modality types and all defects (such as reflexive, symmetric or not weakly connected points) are displayed on the corresponding pages.
On the right side of the window there are pages containing lists of frame defects: items in the lists can be selected and then the arrows are highlighted (using dark blue and dark red, respectively) to show the selected defect. Note that in the case of transitive (and reflexive) modality dashed arrows show defects which have been induced by taking the respective closure of the displayed relation.
Export to TeX in Actions menu allows you to generate LaTeX pictures of the current frame for two different packages: ebezier and pstricks. Note that this facility can only work (due to security restrictions on access to the system clipboard) when the applet is run locally, not from the Internet. See below how to run it locally.
Note: This applet requiresJava Plug-in 1.3 (or higher).
If your browser does not support Java Plug-in, but you have JDK 1.2 or JRE 1.2 (or higher) installed on your computer, you can still use the program: download jar file containing the applet code and three images: red, green and blue. Put the images into subdirectory images and then run the applet executing the command
java -cp products.jar FrameExplorer
Any comments and suggestions please send to Roman Kontchakov.
