Uses of Class
edu.mit.csail.sdg.alloy4.Err

Packages that use Err

edu.mit.csail.sdg.alloy4	This package contains general data structures and helper classes.
edu.mit.csail.sdg.alloy4compiler.ast	This package contains the definition of AST nodes.
edu.mit.csail.sdg.alloy4compiler.parser	This package contains the compiler
edu.mit.csail.sdg.alloy4compiler.sim	This package contains a pure-Java evaluator/simulator for Alloy4 instances.
edu.mit.csail.sdg.alloy4compiler.translator	This package contains the translator from Alloy4 to CNF (using kodkod).
edu.mit.csail.sdg.alloy4viz	This package displays Alloy4 instances.
edu.mit.csail.sdg.alloy4whole	This package contains a simple GUI client, as well as several examples on using the API.

Uses of Err in edu.mit.csail.sdg.alloy4

Subclasses of Err in edu.mit.csail.sdg.alloy4

class	ErrorAPI Immutable; this represents an API usage error.
class	ErrorFatal Immutable; this represents a fatal error.
class	ErrorSyntax Immutable; this represents a syntax error that should be reported to the user.
class	ErrorType Immutable; this represents a type error that should be reported to the user.
class	ErrorWarning Immutable; this represents a nonfatal warning that should be reported to the user.

Methods in edu.mit.csail.sdg.alloy4 that throw Err

static long

Util.writeAll(java.lang.String filename, java.lang.String content) Open then overwrite the file with the given content; throws Err if an error occurred.

Uses of Err in edu.mit.csail.sdg.alloy4compiler.ast

Fields in edu.mit.csail.sdg.alloy4compiler.ast with type parameters of type Err

JoinableList<Err>

Expr.errors The list of errors on this node; nonempty iff this.type==EMPTY

Methods in edu.mit.csail.sdg.alloy4compiler.ast with parameters of type Err

Expr	ExprUnary.Op.make(Pos pos, Expr sub, Err extraError, long extraWeight) Construct an ExprUnary node.

Methods in edu.mit.csail.sdg.alloy4compiler.ast that throw Err

Sig.Field	Sig.addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, java.lang.String label, Expr bound) Add then return a new field F where this.F is bound to an exact "definition" expression.
void	Sig.addFact(Expr fact) Add a new per-atom fact; this expression is allowed to refer to this.decl.get()
Sig.Field	Sig.addField(java.lang.String label, Expr bound) Add then return a new field, where "all x: ThisSig | x.F in bound"
Sig.Field[]	Sig.addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos isDisjoint2, Pos isMeta, java.lang.String[] labels, Expr bound) Add then return a new field, where "all x: ThisSig | x.F in bound"
SafeList<Sig.PrimSig>	Sig.PrimSig.children() Returns its immediate children sigs (not including NONE)
Expr	Expr.comprehensionOver(Decl firstDecl, Decl... moreDecls) Returns the comprehension expression {...|this}
java.lang.Iterable<Sig.PrimSig>	Sig.PrimSig.descendents() Returns its subsigs and their subsigs and their subsigs, etc.
Expr	Expr.forAll(Decl firstDecl, Decl... moreDecls) Returns the formula (all...| this)
Expr	Expr.forLone(Decl firstDecl, Decl... moreDecls) Returns the formula (lone...| this)
Expr	Expr.forNo(Decl firstDecl, Decl... moreDecls) Returns the formula (no...| this)
Expr	Expr.forOne(Decl firstDecl, Decl... moreDecls) Returns the formula (one ...| this)
Expr	Expr.forSome(Decl firstDecl, Decl... moreDecls) Returns the formula (some...| this)
java.util.Set<java.lang.String>	Command.getAllStringConstants(java.lang.Iterable<Sig> sigs) Return a modifiable copy of the set of all String constants used in this command or in any facts embedded in this command.
Decl	Expr.loneOf(java.lang.String label) Return a new declaration "v: lone this"
Decl	Expr.oneOf(java.lang.String label) Return a new declaration "v: one this"
Expr	Module.parseOneExpressionFromString(java.lang.String input) Parse one expression by starting fromt this module as the root module.
void	Func.setBody(Expr newBody) Changes the method body.
Decl	Expr.setOf(java.lang.String label) Return a new declaration "v: set this"
Decl	Expr.someOf(java.lang.String label) Return a new declaration "v: some this"
Expr	Expr.sumOver(Decl firstDecl, Decl... moreDecls) Returns the integer (sum...| this)
Expr	Type.toExpr() Convert this type into a UNION of PRODUCT of sigs.
T	VisitReturn.visit(ExprBad x) Visits a ExprBad node
T	VisitReturn.visit(ExprBadCall x) Visits a ExprBadCall node
T	VisitReturn.visit(ExprBadJoin x) Visits a ExprBadJoin node
abstract T	VisitReturn.visit(ExprBinary x) Visits an ExprBinary node.
T	VisitQuery.visit(ExprBinary x) Visits an ExprBinary node (A OP B) by calling accept() on A then B.
abstract T	VisitReturn.visit(ExprCall x) Visits an ExprCall node.
T	VisitQuery.visit(ExprCall x) Visits an ExprCall node F[X1,X2,X3..] by calling accept() on X1, X2, X3...
abstract T	VisitReturn.visit(ExprConstant x) Visits an ExprConstant node.
T	VisitQuery.visit(ExprConstant x) Visits an ExprConstant node (this default implementation simply returns null)
abstract T	VisitReturn.visit(ExprITE x) Visits an ExprITE node.
T	VisitQuery.visit(ExprITE x) Visits an ExprITE node (C => X else Y) by calling accept() on C, X, then Y.
abstract T	VisitReturn.visit(ExprLet x) Visits an ExprLet node.
T	VisitQuery.visit(ExprLet x) Visits an ExprLet node (let a=x | y) by calling accept() on "a", "x", then "y".
abstract T	VisitReturn.visit(ExprList x) Visits an ExprList node.
T	VisitQuery.visit(ExprList x) Visits an ExprList node F[X1,X2,X3..] by calling accept() on X1, X2, X3...
abstract T	VisitReturn.visit(ExprQt x) Visits an ExprQt node.
T	VisitQuery.visit(ExprQt x) Visits an ExprQt node (all a,b,c:X1, d,e,f:X2...
abstract T	VisitReturn.visit(ExprUnary x) Visits an ExprUnary node.
T	VisitQuery.visit(ExprUnary x) Visits an ExprUnary node (OP X) by calling accept() on X.
abstract T	VisitReturn.visit(ExprVar x) Visits an ExprVar node.
T	VisitQuery.visit(ExprVar x) Visits a ExprVar node (this default implementation simply returns null)
abstract T	VisitReturn.visit(Sig.Field x) Visits a Field node.
T	VisitQuery.visit(Sig.Field x) Visits a Field node (this default implementation simply returns null)
abstract T	VisitReturn.visit(Sig x) Visits a Sig node.
T	VisitQuery.visit(Sig x) Visits a Sig node (this default implementation simply returns null)
T	VisitReturn.visitThis(Expr x) This is the start method that begins a traversal over the given expression.

Constructors in edu.mit.csail.sdg.alloy4compiler.ast with parameters of type Err

ExprBad(Pos pos, java.lang.String originalText, Err error)
Constructs an ExprBad object.

ExprCustom(Pos pos, Err error)
Constructs an ExprCustom object.

Constructors in edu.mit.csail.sdg.alloy4compiler.ast that throw Err

Func(Pos pos, Pos isPrivate, java.lang.String label, java.util.List<Decl> decls, Expr returnDecl, Expr body)
Constructs a new predicate/function.

Func(Pos pos, java.lang.String label, java.util.List<Decl> decls, Expr returnDecl, Expr body)
Constructs a new predicate/function.

Sig.PrimSig(java.lang.String label, Attr... attributes)
Constructs a toplevel non-builtin sig.

Sig.PrimSig(java.lang.String label, Sig.PrimSig parent, Attr... attributes)
Constructs a non-builtin sig.

Sig.SubsetSig(java.lang.String label, java.util.Collection<Sig> parents, Attr... attributes)
Constructs a subset sig.

Uses of Err in edu.mit.csail.sdg.alloy4compiler.parser

Methods in edu.mit.csail.sdg.alloy4compiler.parser that throw Err

Symbol	CompLexer.next_token() Resumes scanning until the next regular expression is matched, the end of input is encountered or an I/O-Error occurs.
static CompModule	CompUtil.parseEverything_fromFile(A4Reporter rep, java.util.Map<java.lang.String,java.lang.String> loaded, java.lang.String filename) Read everything from "file" and parse it; if it mentions submodules, open them and parse them too.
static CompModule	CompUtil.parseEverything_fromFile(A4Reporter rep, java.util.Map<java.lang.String,java.lang.String> loaded, java.lang.String filename, int initialResolutionMode) Read everything from "file" and parse it; if it mentions submodules, open them and parse them too.
static Expr	CompUtil.parseOneExpression_fromString(Module world, java.lang.String input) Parses then typecheck the given input String as an Alloy expression from that world
Expr	CompModule.parseOneExpressionFromString(java.lang.String input) Parse one expression by starting fromt this module as the root module.
static ConstList<Command>	CompUtil.parseOneModule_fromFile(java.lang.String filename) Parses 1 module from the file (without loading any subfiles)
static ConstList<Command>	CompUtil.parseOneModule_fromString(java.lang.String content) Parses 1 module from the input string (without loading any subfiles)
static CompModule	CompUtil.parseOneModule(java.lang.String content)
void	CompParser.syntax_error(Symbol x)

Uses of Err in edu.mit.csail.sdg.alloy4compiler.sim

Methods in edu.mit.csail.sdg.alloy4compiler.sim that throw Err

boolean	SimInstance.cform(Expr x) Convenience method that evalutes x and casts the result to be a boolean.
int	SimInstance.cint(Expr x) Convenience method that evalutes x and cast the result to be a int.
SimTupleset	SimInstance.cset(Expr x) Convenience method that evalutes x and cast the result to be a tupleset
boolean	SimInstance.deleteAtom(SimAtom atom) Delete an atom from all sigs/fields/skolem...
boolean	SimInstance.equal(Expr a, Expr b) Helper method that evaluates the formula "a = b"
void	SimInstance.init(ExprVar var, SimTupleset value) Initializes the given var to be associated with the given unary value; should only be called at the beginning.
void	SimInstance.init(Sig.Field field, SimTupleset value) Initializes the given field to be associated with the given unary value; should only be called at the beginning.
void	SimInstance.init(Sig sig, SimTupleset value) Initializes the given sig to be associated with the given unary value; should only be called at the beginning.
boolean	SimInstance.isIn(Expr a, Expr b) Helper method that evaluates the formula "a in b"
boolean	SimInstance.isIn(SimTuple a, Expr b) Helper method that evaluates the formula "a in b" where b.mult==0
SimAtom	SimInstance.makeAtom(Sig sig) Create a fresh atom for the given sig, then return the newly created atom.
static SimInstance	SimInstance.read(Module root, java.lang.String filename, java.util.List<ExprVar> vars) Construct a new simulation context by reading the given file.
java.lang.Object	SimInstance.visit(ExprBinary x) Visits an ExprBinary node.
java.lang.Object	SimInstance.visit(ExprCall x) Visits an ExprCall node.
java.lang.Object	SimInstance.visit(ExprConstant x) Visits an ExprConstant node.
java.lang.Object	SimInstance.visit(ExprITE x) Visits an ExprITE node.
java.lang.Object	SimInstance.visit(ExprLet x) Visits an ExprLet node.
java.lang.Object	SimInstance.visit(ExprList x) Visits an ExprList node.
java.lang.Object	SimInstance.visit(ExprQt x) Visits an ExprQt node.
java.lang.Object	SimInstance.visit(ExprUnary x) Visits an ExprUnary node.
java.lang.Object	SimInstance.visit(ExprVar x) Visits an ExprVar node.
SimTupleset	SimInstance.visit(Sig.Field x) Visits a Field node.
SimTupleset	SimInstance.visit(Sig x) Visits a Sig node.

Constructors in edu.mit.csail.sdg.alloy4compiler.sim that throw Err

SimInstance(Module root, int bitwidth, int maxseq)
Construct a new simulation context with the given bitwidth and the given maximum sequence length.

SimInstance(SimInstance old)
Construct a deep copy of this instance (except that it shares the same root Module object as the old instance)

Uses of Err in edu.mit.csail.sdg.alloy4compiler.translator

Methods in edu.mit.csail.sdg.alloy4compiler.translator that throw Err

static java.lang.Object	TranslateAlloyToKodkod.alloy2kodkod(A4Solution sol, Expr expr) Translate the Alloy expression into an equivalent Kodkod Expression or IntExpression or Formula object.
kodkod.instance.Instance	A4Solution.debugExtractKInstance() Returns the Kodkod instance represented by this solution; throws an exception if the problem is not yet solved or if it is unsatisfiable.
java.lang.Object	A4Solution.eval(Expr expr) If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean.
static A4Solution	TranslateAlloyToKodkod.execute_command(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
static A4Solution	TranslateAlloyToKodkod.execute_commandFromBook(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
A4Solution	A4Solution.next() If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT).
static A4Solution	A4SolutionReader.read(java.lang.Iterable<Sig> sigs, XMLNode xml) Parse the XML element into an AlloyInstance.
boolean	Simplifier.simplify(A4Reporter rep, A4Solution sol, java.util.List<kodkod.ast.Formula> formulas) Simplify sol.bounds() based on the set of formulas, or to modify the formulas list itself.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprBinary x) Visits an ExprBinary node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprCall x) Visits an ExprCall node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprConstant x) Visits an ExprConstant node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprITE x) Visits an ExprITE node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprLet x) Visits an ExprLet node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprList x) Visits an ExprList node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprQt x) Visits an ExprQt node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprUnary x) Visits an ExprUnary node.
java.lang.Object	TranslateAlloyToKodkod.visit(ExprVar x) Visits an ExprVar node.
java.lang.Object	TranslateAlloyToKodkod.visit(Sig.Field x) Visits a Field node.
java.lang.Object	TranslateAlloyToKodkod.visit(Sig x) Visits a Sig node.
static void	A4SolutionWriter.writeMetamodel(ConstList<Sig> sigs, java.lang.String originalFilename, java.io.PrintWriter out) Write the metamodel as <instance>..</instance> in XML format.
void	A4Solution.writeXML(A4Reporter rep, java.io.PrintWriter writer, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles) Helper method to write out a full XML file.
void	A4Solution.writeXML(A4Reporter rep, java.lang.String filename, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles) Helper method to write out a full XML file.
void	A4Solution.writeXML(java.io.PrintWriter writer, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles) Helper method to write out a full XML file.
void	A4Solution.writeXML(java.lang.String filename) Helper method to write out a full XML file.
void	A4Solution.writeXML(java.lang.String filename, java.lang.Iterable<Func> macros) Helper method to write out a full XML file.
void	A4Solution.writeXML(java.lang.String filename, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles) Helper method to write out a full XML file.

Uses of Err in edu.mit.csail.sdg.alloy4viz

Methods in edu.mit.csail.sdg.alloy4viz that throw Err

static AlloyInstance	StaticInstanceReader.parseInstance(java.io.File file) Parse the file into an AlloyInstance if possible.
static AlloyInstance	StaticInstanceReader.parseInstance(java.io.Reader reader) Parse the file into an AlloyInstance if possible, then close the Reader afterwards.

Uses of Err in edu.mit.csail.sdg.alloy4whole

Methods in edu.mit.csail.sdg.alloy4whole that throw Err

static java.util.Map<java.lang.String,Sig.PrimSig>	Helper.atom2sig(A4Solution solution) Given an A4Solution, return a map that maps every atom to its most specific signature.
static void	ExampleUsingTheCompiler.main(java.lang.String[] args)
static void	ExampleUsingTheAPI.main(java.lang.String[] args)
static void	DemoFileSystem.main(java.lang.String[] args)