A B C D E F G H I J K L M N O P R S T U V W X Y Z _

M

MacUtil - Class in edu.mit.csail.sdg.alloy4

This class provides better integration on Mac OS X.

MailBug - Class in edu.mit.csail.sdg.alloy4

This class asks the user for permission to email a bug report when an uncaught exception occurs.

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4.WorkerEngine

This is the entry point for the sub JVM.

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4whole.DemoFileSystem

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4whole.ExampleUsingTheAPI

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4whole.SimpleCLI

main(String[]) - Static method in class edu.mit.csail.sdg.alloy4whole.SimpleGUI

Main method that launches the program; this method might be called by an arbitrary thread.

main(String[]) - Static method in class tmp.KK

main(String[]) - Static method in class tmp.Ok

main(String[]) - Static method in class tmp.Test

main(String[]) - Static method in class tmp.Test1

main(String[]) - Static method in class tmp.TestSlow

main(String[]) - Static method in class tmp.TestSmallFast

main(String[]) - Static method in class tmp.TestSmallSlow

make() - Static method in class edu.mit.csail.sdg.alloy4.ConstList

Return an unmodifiable empty list.

make(int, T) - Static method in class edu.mit.csail.sdg.alloy4.ConstList

Return an unmodifiable list consisting of "n" references to "elem".

make(Iterable<T>) - Static method in class edu.mit.csail.sdg.alloy4.ConstList

Return an unmodifiable list with the same elements as the given collection.

make() - Static method in class edu.mit.csail.sdg.alloy4.ConstMap

Returns an unmodifiable empty map.

make(Map<K, V>) - Static method in class edu.mit.csail.sdg.alloy4.ConstMap

Returns an unmodifiable map with the same entries and traversal order as the given map.

make() - Static method in class edu.mit.csail.sdg.alloy4.ConstSet

Returns an unmodifiable empty set.

make(Iterable<K>) - Static method in class edu.mit.csail.sdg.alloy4.ConstSet

Returns an unmodifiable set with the same elements and traversal order as the given set.

make(JoinableList<E>) - Method in class edu.mit.csail.sdg.alloy4.JoinableList

Returns a list that represents the concatenation of this list and that list.

make(E) - Method in class edu.mit.csail.sdg.alloy4.JoinableList

Returns a list that represents the result of appending newItem onto this list; if newItem==null we return this list as-is.

make(X, Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Assign the given attributes to the given JComponent, then return the JComponent again.

make(String) - Method in class edu.mit.csail.sdg.alloy4.UniqueNameGenerator

Generate a unique name based on the input name.

make(Pos) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.Attr.AttrType

Construct an attribute of this type with this position; if pos==null, it is treated as Pos.UNKNOWN.

make(Pos, Pos, String, Browsable) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

Construct a Browsable node with the given HTML description and the given single subnode.

make(String, Browsable) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

Construct a Browsable node with the given HTML description and the given single subnode.

make(String, List<? extends Browsable>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

Construct a Browsable node with the given HTML description and the given 0 or more subnodes.

make(Pos, Pos, String, List<? extends Browsable>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.Browsable

Construct a Browsable node with the given HTML description and the given 0 or more subnodes.

make(Pos, Pos, Func, ConstList<Expr>, long) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprBadCall

Constructs an ExprBadCall object.

make(Pos, Pos, Expr, Expr) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprBadJoin

Constructs an ExprBadJoin node.

make(Pos, Pos, Expr, Expr) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprBinary.Op

Constructs a new ExprBinary node.

make(Pos, Pos, Func, List<Expr>, long) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprCall

Constructs an ExprCall node with the given predicate/function "fun" and the list of arguments "args".

make(Pos, ConstList<Expr>, ConstList<String>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprChoice

Construct an ExprChoice node.

make(Pos, int) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant.Op

Makes an ExprConstant node

make(Pos, String) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant.Op

Makes an ExprConstant node

make(Pos, Expr, Expr, Expr) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprITE

Constructs a ExprITE expression.

make(Pos, ExprVar, Expr, Expr) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprLet

Constructs a LET expression.

make(Pos, Pos, ExprList.Op, List<? extends Expr>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprList

Generates a call to a builtin predicate

make(Pos, Pos, List<Decl>, Expr) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprQt.Op

Constructs a quantification expression with "this" as the operator.

make(Pos, Expr) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprUnary.Op

Construct an ExprUnary node.

make(Pos, Expr, Err, long) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.ExprUnary.Op

Construct an ExprUnary node.

make(Pos, String) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

Constructs an ExprVar variable with the EMPTY type

make(Pos, String, Type) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

Constructs an ExprVar variable with the given type

make(String) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimAtom

Construct a SimAtom for the given label, or if an existing SimAtom hasn't been garbage collected yet then return that instead.

make(int) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimAtom

Construct a SimAtom for the given integer, or if an existing SimAtom hasn't been garbage collected yet then return that instead.

make(long) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimAtom

Construct a SimAtom for the given integer, or if an existing SimAtom hasn't been garbage collected yet then return that instead.

make(List<SimAtom>) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTuple

Construct the n-ary tuple; throws an exception if the given list is empty.

make(SimAtom, SimAtom) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTuple

Construct the binary tuple (a,b)

make(SimAtom) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTuple

Construct the unary tuple containing the given atom.

make(String) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTuple

Construct the unary tuple containing the given atom.

make(String[]) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTuple

Construct the tuple containing the given list of atoms; the list must not be empty.

make(int, int) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTupleset

Construct the set containing integers between min and max (inclusively).

make(SimTuple) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTupleset

Construct a tupleset containing the given tuple.

make(String) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTupleset

Make a tupleset containing the given atom.

make(Collection<SimTuple>) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTupleset

Make a tupleset containing a deep copy of the given list of tuples (Note: caller MUST make sure there are no duplicates, and all tuples are of same arity!)

make(String, String, String, String[]) - Static method in class edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver

Constructs a new SatSolver value that uses a command-line solver; throws ErrorAPI if the ID is already in use.

make(String, String, String) - Static method in class edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver

Constructs a new SatSolver value that uses a command-line solver; throws ErrorAPI if the ID is already in use.

makeAND(Pos, Pos, Expr, Expr) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprList

Generates the expression (arg1 and arg2)

makeAtom(Sig) - Method in class edu.mit.csail.sdg.alloy4compiler.sim.SimInstance

Create a fresh atom for the given sig, then return the newly created atom.

makeConst() - Method in class edu.mit.csail.sdg.alloy4.ConstList.TempList

Makes this TempList unmodifiable, then construct a ConstList backed by this TempList.

makeConstList() - Method in class edu.mit.csail.sdg.alloy4.SafeList

Constructs an unmodifiable ConstList containing the same elements as this list.

makeCopy() - Method in class edu.mit.csail.sdg.alloy4.SafeList

Constructs a modifiable ArrayList containing the same elements as this list.

makeDISJOINT(Pos, Pos, List<? extends Expr>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprList

Generates the expression disj[arg1, args2, arg3...]

makeH(Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Make a JPanel using horizontal BoxLayout, and add the components to it (each component will be center-aligned).

makeHB(Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Make a JPanel using horizontal BoxLayout, and add the components to it (each component will be bottom-aligned).

makeHT(Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Make a JPanel using horizontal BoxLayout, and add the components to it (each component will be top-aligned).

makenext(int, int) - Static method in class edu.mit.csail.sdg.alloy4compiler.sim.SimTupleset

Construct the set containing (min,min+1)...(max-1,max)

makenull(Pos) - Method in enum edu.mit.csail.sdg.alloy4compiler.ast.Attr.AttrType

Construct an attribute of this type with this position; if pos==null, this method returns null.

makeNUMBER(int) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant

Constructs the integer "n"

makeOR(Pos, Pos, Expr, Expr) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprList

Generates the expression (arg1 || arg2)

makeTOTALORDER(Pos, Pos, List<? extends Expr>) - Static method in class edu.mit.csail.sdg.alloy4compiler.ast.ExprList

Generates the expression pred/totalOrder[arg1, args2, arg3...]

makeVL(Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Make a JPanel using vertical BoxLayout, and add the components to it (each component will be left-aligned).

makeVR(Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Make a JPanel using vertical BoxLayout, and add the components to it (each component will be right-aligned).

max(int) - Static method in class edu.mit.csail.sdg.alloy4.Util

Returns the largest allowed integer, or -1 if no integers are allowed (bitwidth < 1).

MAX - Static variable in class edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant

The largest integer value allowed by the current bitwidth.

max() - Method in class edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

Returns the largest allowed integer, or -1 if no integers are allowed.

maxseq - Variable in class edu.mit.csail.sdg.alloy4compiler.ast.Command

The maximum sequence length (0 or higher) (Or -1 if it was not specified).

maxstring - Variable in class edu.mit.csail.sdg.alloy4compiler.ast.Command

The number of String atoms to allocate (0 or higher) (Or -1 if it was not specified).

menu(JMenuBar, String, Runnable) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Construct a new JMenu and add it to an existing JMenuBar.

menuCanceled(MenuEvent) - Method in class edu.mit.csail.sdg.alloy4.Runner

This method is defined in javax.swing.event.MenuListener; (this implementation does nothing)

menuDeselected(MenuEvent) - Method in class edu.mit.csail.sdg.alloy4.Runner

This method is defined in javax.swing.event.MenuListener; (this implementation does nothing)

menuItem(JMenu, String, Object...) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

Construct a new JMenuItem then add it to an existing JMenu.

menuSelected(MenuEvent) - Method in class edu.mit.csail.sdg.alloy4.Runner

This method is defined in javax.swing.event.MenuListener; (this implementation calls this.run())

merge(Pos) - Method in class edu.mit.csail.sdg.alloy4.Pos

Return a new position that merges this and that (it is assumed that the two Pos objects have same filename)

merge(Type) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Type

Returns a new type { A | A is in this, or A is in that }

merge(Type.ProductType) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Type

Returns a new type { A | A is in this, or A == that }

merge(Type.ProductType, int, int) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Type

Returns a new type { A | A is in this, or A == that.subList(begin,end) }

merge(List<Sig.PrimSig>) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Type

Returns a new type { A | A is in this, or A == that }

mergeArrows - Variable in class edu.mit.csail.sdg.alloy4viz.VizState

META - Static variable in class edu.mit.csail.sdg.alloy4compiler.ast.Attr

META; if a Sig has the META attribute, it means it is a META atom corresponding to some real signature or field.

metaField() - Method in class edu.mit.csail.sdg.alloy4compiler.parser.CompModule

Returns the meta signature "field$" (or null if such a sig does not exist)

metaSig() - Method in class edu.mit.csail.sdg.alloy4compiler.parser.CompModule

Returns the meta signature "sig$" (or null if such a sig does not exist)

min(int) - Static method in class edu.mit.csail.sdg.alloy4.Util

Returns the smallest allowed integer, or 0 if no integers are allowed (bitwidth < 1)

MIN - Static variable in class edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant

The smallest integer value allowed by the current bitwidth.

min() - Method in class edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

Returns the smallest allowed integer, or 0 if no integers are allowed

minimize(JFrame) - Static method in class edu.mit.csail.sdg.alloy4.OurUtil

This method minimizes the window.

minimized(Object, int, int) - Method in class edu.mit.csail.sdg.alloy4.A4Reporter

If solver!=KK and solver!=CNF, this method is called by the translator after performing the unsat core minimization.

minimizing(Object, int) - Method in class edu.mit.csail.sdg.alloy4.A4Reporter

If solver!=KK and solver!=CNF, this method is called by the translator before starting the unsat core minimization.

MiniSatJNI - Static variable in class edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver

MiniSat1 via JNI

MiniSatProverJNI - Static variable in class edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver

MiniSatProver1 via JNI

minus(Expr) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Expr

Returns the expression (this-x)

MINUS - Static variable in class edu.mit.csail.sdg.alloy4compiler.parser.CompSym

minus(A4TupleSet) - Method in class edu.mit.csail.sdg.alloy4compiler.translator.A4TupleSet

Construct a new tupleset as the subtraction of this and that; this and that must be come from the same solution.

model - Variable in class edu.mit.csail.sdg.alloy4viz.AlloyInstance

The AlloyModel that this AlloyInstance is an instance of.

modified() - Method in class edu.mit.csail.sdg.alloy4.OurSyntaxWidget

Returns the modified-or-not flag.

modified(int) - Method in class edu.mit.csail.sdg.alloy4.OurTabbedSyntaxWidget

True if the i-th text buffer has been modified since it was last loaded/saved

Module - Interface in edu.mit.csail.sdg.alloy4compiler.ast

This interface represents an Alloy module.

MODULE - Static variable in class edu.mit.csail.sdg.alloy4compiler.parser.CompSym

moveCaret(int, int) - Method in class edu.mit.csail.sdg.alloy4.OurSyntaxWidget

Select the content between offset a and offset b, and move the caret to offset b.

msg - Variable in exception edu.mit.csail.sdg.alloy4.Err

The actual error message (never null)

mul(Expr) - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Expr

Returns the formula "this.mul[x]" (the result of multiplying this by x)

mult - Variable in class edu.mit.csail.sdg.alloy4compiler.ast.Expr

This field records whether the node is a multiplicity constraint.

mult() - Method in class edu.mit.csail.sdg.alloy4compiler.ast.Expr

If this is loneOf/oneOf/someOf/exactlyOf expression, return loneOf/oneOf/someOf/exactlyOf, otherwise returns setOf.